awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
inr :
  ∀ (pf : l₁ < i) (pf_1 : l₁ ∈ Set.Iic l₁) (pf_2 : l₂ < i) (pf_3 : l₂ ∈ Set.Iic l₂) (pf_4 : l₁ ≤ l₂) (pf_5 : l₁ ≤ l₁)
    (pf_6 : l₂ ≤ l₂) (pf_7 : l₁ ∈ Set.Iic i) (pf_8 : l₂ ∈ Set.Iic i)
    (pf_9 :
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_8),
    Arrow.mk ((iter l₁ pf).mapObj (iter l₂ pf_2) pf_4 pf_5 pf_6 pf_4) = Arrow.mk ((functor hj iter).map (homOfLE pf_9))
⊢ Arrow.mk (X := (iter l₁ ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₁) l₁ ⋯)) (Y :=
      (iter l₂ ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₂) l₂ ⋯))
      ((iter l₁ ⋯).mapObj (iter l₂ ⋯) ⋯ ⋯ ⋯ ⋯) =
    Arrow.mk ((functor hj iter).map (homOfLE ⋯))

Tactic:
generalize_proofs
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
pf : l₁ < i
pf_1 : l₁ ∈ Set.Iic l₁
pf_2 : l₂ < i
pf_3 : l₂ ∈ Set.Iic l₂
pf_4 : l₁ ≤ l₂
pf_5 : l₁ ≤ l₁
pf_6 : l₂ ≤ l₂
pf_7 : l₁ ∈ Set.Iic i
pf_8 : l₂ ∈ Set.Iic i
pf_9 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_8
inr :
  Arrow.mk ((iter l₁ pf).mapObj (iter l₂ pf_2) pf_4 pf_5 pf_6 pf_4) =
    arrowMap (functor hj iter) (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J)
      (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_8) : J) pf_9 pf_8
inr₁ :
  arrowMap (iter l₂ pf_2).F l₁ l₂ pf_4 pf_6 =
    arrowMap (functor hj iter) (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J)
      (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_8) : J) pf_9 pf_8
inr₂ :
  arrowMap (iter l₂ pf_2).F l₁ l₂ pf_4 pf_6 =
    Arrow.mk (X :=
      Functor.obj (C := (↑(Set.Iic (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J)) : Type u))
        (F (iter (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J))
          (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J) ⋯))
      (Y := (iter l₂ hl₂).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₂) l₂ ⋯))
      (mapObj (iter (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J) ⋯) (iter l₂ hl₂) pf_9 ⋯ ⋯ pf_9)
inr₃ inr₄ :
  arrowMap (iter l₂ pf_2).F l₁ l₂ pf_4 pf_6 =
    arrowMap (iter l₂ hl₂).F (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J) l₂ pf_9 ⋯
⊢ Arrow.mk ((iter l₁ pf).mapObj (iter l₂ pf_2) pf_4 pf_5 pf_6 pf_4) = Arrow.mk ((functor hj iter).map (homOfLE pf_9))

Tactic:
rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
simpa using hi
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : IsMin i
isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Nonempty (Iteration.{u, v_1, u_1} (J := J) Φ ⊥)
⊢ Nonempty (Φ.Iteration i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
hi : IsMin.{u} (α := J) ⊥
⊢ Nonempty (Iteration.{u, v_1, u_1} (J := J) Φ ⊥)

Tactic:
⟨mkOfBot Φ J⟩

Premises used: Nonempty.intro, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
hi : IsMin.{u} (α := J) ⊥
⊢ Nonempty (Iteration.{u, v_1, u_1} (J := J) Φ ⊥)

Tactic:
exact ⟨mkOfBot Φ J⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : ¬IsMax i
hi' : Nonempty (Φ.Iteration i)
⊢ Nonempty (Φ.Iteration (Order.succ i))

Tactic:
⟨mkOfSucc hi hi'.some⟩

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfSucc, Nonempty.some, Nonempty.intro
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : ¬IsMax i
hi' : Nonempty (Φ.Iteration i)
⊢ Nonempty (Φ.Iteration (Order.succ i))

Tactic:
exact ⟨mkOfSucc hi hi'.some⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Nonempty (Φ.Iteration b)
⊢ Nonempty (Φ.Iteration i)

Tactic:
⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩

Premises used: Nonempty.some, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit, Nonempty.intro
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Nonempty (Φ.Iteration b)
⊢ Nonempty (Φ.Iteration i)

Tactic:
exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
isMin : ∀ (i : J) (hi : IsMin i), Nonempty (Φ.Iteration i)
succ : ∀ (i : J) (hi : ¬IsMax i) (hi' : Nonempty (Φ.Iteration i)), Nonempty (Φ.Iteration (Order.succ i))
isSuccLimit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hi' : ∀ b < i, Nonempty (Φ.Iteration b)), Nonempty (Φ.Iteration i)
⊢ Nonempty (Φ.Iteration j)

Tactic:
induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
      obtain rfl : i = ⊥ := by simpa using hi
      exact ⟨mkOfBot Φ J⟩
  | succ i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩
  | isSuccLimit i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩

Premises used: CategoryTheory.SmallObject.SuccStruct.succ, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
rw : Eq (α := F.obj ⊥ ⟶ Y) ((F.map (homOfLE ⋯) ≫ sq'.f') ≫ p) (c.ι.app ⊥ ≫ g)
rw₁ : Eq (α := F.obj ⊥ ⟶ Y) (F.map (homOfLE ⋯) ≫ sq'.f' ≫ p) (c.ι.app ⊥ ≫ g)
rw₂ : Eq (α := F.obj ⊥ ⟶ Y) (F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g) (c.ι.app ⊥ ≫ g)
rw₃ rw₄ : Eq (α := F.obj ⊥ ⟶ Y) (c.ι.app ⊥ ≫ g) (c.ι.app ⊥ ≫ g)
⊢ f ≫ p = c.ι.app ⊥ ≫ g

Tactic:
rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.w_assoc, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
inst_3 : SuccOrder J
⊢ sq'.f' ≫ p = CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (c.ι.app (Order.succ j) ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
rw : F.map (homOfLE ⋯ ≫ α) ≫ sq'.f' = f
⊢ F.map (homOfLE ⋯) ≫ F.map α ≫ sq'.f' = f

Tactic:
rw [← F.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯ ≫ α) ≫ sq'.f' = f

Tactic:
sq'.w₁

Premises used: CategoryTheory.homOfLE, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯ ≫ α) ≫ sq'.f' = f

Tactic:
exact sq'.w₁

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
⊢ SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
                sqFunctor c p f g_1)
              g.op) :
          (a : (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i'))) →
            (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i)))
        ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i'))) =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f'

Tactic:
have := congr_arg SqStruct.f' (s.2 g.op)
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
this :
  SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
                sqFunctor c p f g_1)
              g.op) :
          (a : (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i'))) →
            (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i)))
        ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i'))) =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f'
dsimp :
  F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        i ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) i')
    (Functor.map
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        g ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i')).f')
    (((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f' ≫
      Functor.map (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) g)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
this :
  F.map (Functor.map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f'
rw :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X
rw₁ rw₂ :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f'
⊢ F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X

Tactic:
rw [this, comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
i : J
hi : i < j
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
        (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))).f'

Tactic:
(F.isColimitOfIsWellOrderContinuous j hj).fac _ ⟨i, hi⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, Subtype.mk
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
hj : Order.IsSuccLimit.{w} (α := J) ⊥
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
              ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
⊢ False

Tactic:
Order.not_isSuccLimit_bot hj

Premises used: Order.not_isSuccLimit_bot
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
hj : Order.IsSuccLimit.{w} (α := J) ⊥
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iio ⊥) x) :
                (a : { x : J // x ∈ Set.Iio ⊥ }) → J))
              ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
⊢ False

Tactic:
exact Order.not_isSuccLimit_bot hj

Premises used: Order.not_isSuccLimit_bot
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
⊢ ⊥ < j

Tactic:
have h : ⊥ < j := Ne.bot_lt' (by
      rintro rfl
      exact Order.not_isSuccLimit_bot hj)
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
h : ⊥ < j
rw :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
        (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) ⊥ h))).f' =
    f
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f

Tactic:
rw [liftHom_fac hj s ⊥ h]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, Bot.bot
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
h : ⊥ < j
⊢ ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
        (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) ⊥ h))).f' =
    f

Tactic:
simpa using (s.1 ⟨⊥, h⟩).w₁

Premises used: Bot.bot, Subtype.mk, Opposite.op, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁, Subtype.val
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
⊢ ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    c.ι.app
        (Opposite.unop
          (Functor.obj
            (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯))
            (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij)))) ≫
      g

Tactic:
have := (s.1 ⟨i, hij⟩).w₂