awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowι (restrictionLT (iter i hij).F ⋯) hi k hk = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk
have inl : restrictionLT (iter i hij).F sorry = restrictionLT (functor hj iter) hij_1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ restrictionLT (iter i hij).F ⋯ = restrictionLT (functor hj iter) hij_1
have inl : ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
  (restrictionLT (iter i hij).F sorry).mapArrow.obj (Arrow.mk f) =
    (restrictionLT (functor hj iter) hij_1).mapArrow.obj (Arrow.mk f)
Tactic: apply Arrow.functor_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
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₂
⊢ (restrictionLT (iter i hij).F ⋯).mapArrow.obj (Arrow.mk f) =
    (restrictionLT (functor hj iter) hij_1).mapArrow.obj (Arrow.mk f)
have inl : Arrow.mk (X := (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ sorry)) (Y :=
    (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ sorry))
    ((iter i hij).F.map (homOfLE sorry) :
      (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ sorry) ⟶
        (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ sorry)) =
  Arrow.mk ((functor hj iter).map (homOfLE sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
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₂
⊢ Arrow.mk (X := (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯)) (Y :=
      (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯))
      ((iter i hij).F.map (homOfLE ⋯) :
        (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯) ⟶
          (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯)) =
    Arrow.mk ((functor hj iter).map (homOfLE ⋯))
have inl : ∀ (pf : l₁ ∈ Set.Iic i) (pf_1 : l₂ ∈ Set.Iic i)
  (pf_2 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1)
  (pf_3 : l₁ ∈ Set.Iic j) (pf_4 : l₂ ∈ Set.Iic j)
  (pf_5 :
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₁ pf_3 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₂ pf_4),
  Arrow.mk ((iter i hij).F.map (homOfLE pf_2)) = Arrow.mk ((functor hj iter).map (homOfLE pf_5))
Tactic: generalize_proofs
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
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₁ ∈ Set.Iic i
pf_1 : l₂ ∈ Set.Iic i
pf_2 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1
pf_3 : l₁ ∈ Set.Iic j
pf_4 : l₂ ∈ Set.Iic j
pf_5 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₁ pf_3 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₂ pf_4
⊢ Arrow.mk ((iter i hij).F.map (homOfLE pf_2)) = Arrow.mk ((functor hj iter).map (homOfLE pf_5))
have inl : arrowMap (iter i hij).F (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf) : J)
    (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1) : J) pf_2 pf_1 =
  arrowMap (iter l₂ sorry).F l₁ l₂ pf_5 sorry
Tactic: rw [← arrowMap, ← arrowMap, arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij),
        arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
have inr : arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk
Tactic: rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk
have inr : inductiveSystem iter = restrictionLT (functor hj iter) hij
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ inductiveSystem iter = restrictionLT (functor hj iter) hij
have inr : ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
  (inductiveSystem iter).mapArrow.obj (Arrow.mk f) = (restrictionLT (functor hj iter) hij).mapArrow.obj (Arrow.mk f)
Tactic: apply Arrow.functor_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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₂
⊢ (inductiveSystem iter).mapArrow.obj (Arrow.mk f) = (restrictionLT (functor hj iter) hij).mapArrow.obj (Arrow.mk f)
have inr : Arrow.mk (X := (iter l₁ sorry).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₁) l₁ sorry)) (Y :=
    (iter l₂ sorry).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₂) l₂ sorry)) ((iter l₁ sorry).mapObj (iter l₂ sorry) sorry sorry sorry sorry) =
  Arrow.mk ((functor hj iter).map (homOfLE sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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₂
⊢ 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 ⋯))
have 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))
Tactic: generalize_proofs
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ 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))
have 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
Tactic: rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ 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))
have 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
Tactic: rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ 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))
have 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) sorry))
      (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) sorry))
    (Y := (iter l₂ hl₂).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₂) l₂ sorry))
    (mapObj (iter (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf_7) : J) sorry) (iter l₂ hl₂) pf_9 sorry sorry pf_9)
Tactic: rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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)
⊢ 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))
have 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 sorry
Tactic: rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ Nonempty (Φ.Iteration i)
have isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Nonempty (Iteration.{u, v_1, u_1} (J := J) Φ ⊥)
Tactic: obtain rfl : i = ⊥ := by simpa using hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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
⊢ Nonempty (Φ.Iteration j)
have isMin : ∀ (i : J) (hi : IsMin i), Nonempty (Φ.Iteration i)
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)⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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)
⊢ Nonempty (Φ.Iteration j)
have succ : ∀ (i : J) (hi : ¬IsMax i) (hi' : Nonempty (Φ.Iteration i)), Nonempty (Φ.Iteration (Order.succ i))
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)⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (goal)
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))
⊢ Nonempty (Φ.Iteration j)
have isSuccLimit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hi' : ∀ b < i, Nonempty (Φ.Iteration b)), Nonempty (Φ.Iteration i)
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)⟩
Cleared hypotheses: 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
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ f ≫ p = c.ι.app ⊥ ≫ g
have rw : Eq (α := F.obj ⊥ ⟶ Y) ((F.map (homOfLE sorry) ≫ sq'.f') ≫ p) (c.ι.app ⊥ ≫ g)
Tactic: rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_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
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)
⊢ f ≫ p = c.ι.app ⊥ ≫ g
have rw₁ : Eq (α := F.obj ⊥ ⟶ Y) (F.map (homOfLE sorry) ≫ sq'.f' ≫ p) (c.ι.app ⊥ ≫ g)
Tactic: rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_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
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)
⊢ f ≫ p = c.ι.app ⊥ ≫ g
have rw₂ : Eq (α := F.obj ⊥ ⟶ Y) (F.map (homOfLE sorry) ≫ c.ι.app j ≫ g) (c.ι.app ⊥ ≫ g)
Tactic: rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_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
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)
⊢ f ≫ p = c.ι.app ⊥ ≫ g
have rw₃ : Eq (α := F.obj ⊥ ⟶ Y) (c.ι.app ⊥ ≫ g) (c.ι.app ⊥ ≫ g)
Tactic: rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_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
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯) ≫ F.map α ≫ sq'.f' = f
have rw : F.map (homOfLE sorry ≫ α) ≫ sq'.f' = f
Tactic: rw [← F.map_comp_assoc]