isColimitToLinearOrder — Mathlib

Lean4

/-- If `ι` is a linearly ordered type, `I : MultispanIndex (.prod ι) C`, and
`c` a colimit multicofork for `I`, then `c.toLinearOrder` is a colimit
multicofork for `I.toLinearOrder`. -/
def isColimitToLinearOrder (c : Multicofork I) (hc : IsColimit c) (h : I.SymmStruct) : IsColimit c.toLinearOrder :=
  Multicofork.IsColimit.mk _ (fun s ↦ hc.desc (ofLinearOrder s h)) (fun s _ ↦ hc.fac (ofLinearOrder s h) _)
    (fun s m hm ↦
      Multicofork.IsColimit.hom_ext hc
        (fun i ↦ by
          have := hc.fac (ofLinearOrder s h) (.right i)
          dsimp at this
          rw [this]
          apply hm))

Похожие утверждения