awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this_1 :
  ∀ (sq : CommSq (Y := F.obj (Order.succ j)) sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯))
    (F.map (homOfLE ⋯) ≫ sq'.f')
have conv_rhs : Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE sorry)) (CommSq.lift sorry))
  (CategoryStruct.comp (Y := F.obj (Order.succ (Opposite.unop (Opposite.op j)))) (F.map (homOfLE sorry ≫ homOfLE sorry))
    (CommSq.lift sorry))
Tactic: conv_rhs => rw [← sq'.sq.fac_left, ← F.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
⊢ sq.HasLift
have obtain : ∀ (s : (↑(sqFunctor c p f g).sections : Type (max w v)))
  (hs :
    ((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
          Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
        s =
      { f' := f, w₁ := sorry, w₂ := sorry : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }),
  sq.HasLift
Tactic: obtain ⟨s, hs⟩ := (wellOrderInductionData c f g hF).surjective { w₂ := sq.w, .. }
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs :
  ((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
        Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
      s =
    { f' := f, w₁ := ⋯, w₂ := ⋯ : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }
⊢ sq.HasLift
have hs₁ : SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g)
    (((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
        Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
      s) =
  { f' := f, w₁ := sorry, w₂ := sorry : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }.f'
Tactic: replace hs := congr_arg SqStruct.f' hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
⊢ sq.HasLift
have hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
Tactic: have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
rw : ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op ⊥)).f' = f
⊢ c.ι.app ⊥ ≫ l = f
have rw₁ : f = f
Tactic: rw [hl, hs]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
j : J
⊢ c.ι.app j ≫ l ≫ p = c.ι.app j ≫ g
have rw : ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f' ≫ p = c.ι.app j ≫ g
Tactic: rw [reassoc_of% (hl j), SqStruct.w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
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
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
j : J
rw : ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f' ≫ p = c.ι.app j ≫ g
⊢ c.ι.app j ≫ l ≫ p = c.ι.app j ≫ g
have rw₁ : c.ι.app j ≫ g = c.ι.app j ≫ g
Tactic: rw [reassoc_of% (hl j), SqStruct.w₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
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
inst_3 : F.IsWellOrderContinuous
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p
f : F.obj ⊥ ⟶ X
g : Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) ⊥ ⟶ Y
sq : CommSq f (c.ι.app ⊥) p g
j : J
hj : ¬IsMax j
x : F.obj j ⟶ X
h : CommSq x (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ h.HasLift
have this : HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE sorry)) p
Tactic: have := hF j hj
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ W.llp.IsStableUnderTransfiniteCompositionOfShape J
have rw : W.llp.transfiniteCompositionsOfShape J ≤ W.llp
Tactic: rw [isStableUnderTransfiniteCompositionOfShape_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
⊢ W.llp f
have this : W.llp (X := h.toTransfiniteCompositionOfShape (W := W.llp).F.obj ⊥)
  (h.toTransfiniteCompositionOfShape (W := W.llp).incl.app ⊥)
Tactic: have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
      (hc := h.isColimit) (fun j hj ↦ h.map_mem j hj _ hp)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp
have this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
Tactic: have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp
have this₁ : W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp
Tactic: rw [isStableUnderTransfiniteCompositionOfShape_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ ((coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp
have rw : (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp
Tactic: rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W f
⊢ W.rlp.llp f
have hf₁ : ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
  W.transfiniteCompositionsOfShape J f
Tactic: rw [transfiniteCompositions_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f
⊢ W.rlp.llp f
have obtain : ∀ (w : Type w) (w_1 : LinearOrder w) (w_2 : SuccOrder w) (w_3 : OrderBot w) (w_4 : WellFoundedLT w)
  (hf : W.transfiniteCompositionsOfShape w f), W.rlp.llp f
Tactic: obtain ⟨_, _, _, _, _, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts).retracts ≤ W.rlp.llp
have rw : transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp
Tactic: rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk (X := Functor.obj (Φ.iterationFunctor J) i₁) (Functor.map (Φ.iterationFunctor J) (homOfLE h₁₂)) =
    Arrow.mk (iter.F.map (homOfLE h₁₂))
have dsimp : Arrow.mk (X :=
    Functor.obj (C := (↑(Set.Iic i₁) : Type w)) (Iteration.F (Φ.iter i₁))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₁) i₁ sorry))
    (Y :=
    Functor.obj (C := (↑(Set.Iic i₂) : Type w)) (Iteration.F (Φ.iter i₂))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₂) i₂ sorry))
    (Iteration.mapObj (Φ.iter i₁) (Φ.iter i₂) sorry sorry sorry sorry) =
  Arrow.mk (iter.F.map (homOfLE h₁₂))
Tactic: dsimp [iterationFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk (X :=
      Functor.obj (C := (↑(Set.Iic i₁) : Type w)) (Iteration.F (Φ.iter i₁))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₁) i₁ ⋯))
      (Y :=
      Functor.obj (C := (↑(Set.Iic i₂) : Type w)) (Iteration.F (Φ.iter i₂))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₂) i₂ ⋯))
      (Iteration.mapObj (Φ.iter i₁) (Φ.iter i₂) ⋯ ⋯ ⋯ ⋯) =
    Arrow.mk (iter.F.map (homOfLE h₁₂))
have rw : arrowMap (Iteration.F (Φ.iter i₂)) i₁ i₂ sorry sorry = Arrow.mk (iter.F.map (homOfLE h₁₂))
Tactic: rw [Iteration.arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
⊢ IsColimit (J := (↑(Set.Iio i) : Type w)) (F :=
    Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
              x1 < x2) (Set.principalSegIio i)) :
          (a : (↑(Set.Iio i) : Type w)) → J))
        ⋯ ⋙
      Φ.iterationFunctor J)
    (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))
have refine : IsColimit ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J)))
Tactic: refine (IsColimit.precomposeInvEquiv e _).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
⊢ IsColimit ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J)))
have refine : coconeOfLE (Iteration.F (Φ.iter i)) sorry ≅
  (Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))
Tactic: refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
⊢ coconeOfLE (Iteration.F (Φ.iter i)) ⋯ ≅
    (Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))
have refine : ∀ (j : (↑(Set.Iio i) : Type w)),
  CategoryStruct.comp (Y :=
      Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) sorry)
        (coconeOfLE (Iteration.F (Φ.iter i)) sorry))
      (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) sorry)) j :
        Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) j ⟶
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
              (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) sorry)
                (coconeOfLE (Iteration.F (Φ.iter i)) sorry)))
            j)
      (Iso.hom (eqToIso sorry)) =
    ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app j
Tactic: refine Cocone.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
        (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
      (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) :
        Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
              (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
                (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      (Iso.hom (eqToIso ⋯)) =
    ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)
have a : Arrow.mk (X :=
    Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) (Y :=
    ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).pt)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) sorry)
        (coconeOfLE (Iteration.F (Φ.iter i)) sorry))
      (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) sorry))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) :
        Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
              (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) sorry)
                (coconeOfLE (Iteration.F (Φ.iter i)) sorry)))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      (Iso.hom (eqToIso sorry))) =
  Arrow.mk (X :=
    Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
    (((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
Tactic: apply Arrow.mk_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
x x_1 : J
f : x ⟶ x_1
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) Φ.X₀) x ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (Functor.map (Functor.obj (Functor.const J) Φ.X₀) f ≫
      Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) ≫
      Functor.map (Φ.iterationFunctor J) f)
have dsimp : Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
  (𝟙 Φ.X₀ ≫ Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE sorry))
  ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE sorry)) ≫
    Functor.map (Φ.iterationFunctor J) f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (𝟙 Φ.X₀ ≫ Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) ≫
      Functor.map (Φ.iterationFunctor J) f)
have rw : Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
  (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE sorry))
  (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE sorry ≫ f))
Tactic: rw [id_comp, assoc, ← Functor.map_comp]