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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ restrictionLT iter.F hij' =
    restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
      hij
have e_F : ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
  (restrictionLT iter.F hij').mapArrow.obj (Arrow.mk f) =
    (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))))
            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
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
⊢ (restrictionLT iter.F hij').mapArrow.obj (Arrow.mk f) =
    (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
            hij).mapArrow.obj
      (Arrow.mk f)
have e_F : Arrow.mk (iter.F.map (homOfLE sorry)) =
  Arrow.mk (X :=
    obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
      (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) k₁ sorry))
    (map (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))))
      (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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
⊢ Arrow.mk (iter.F.map (homOfLE ⋯)) =
    Arrow.mk (X :=
      obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) k₁ ⋯))
      (map (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (homOfLE ⋯))
have e_F : arrowMap iter.F (↑(sorry.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
    (↑(sorry.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) sorry sorry =
  arrowMap iter.F (↑(sorry.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
    (↑(sorry.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) sorry sorry
Tactic: rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc]
-- 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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
e_F :
  arrowMap iter.F (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
      (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ⋯ ⋯ =
    arrowMap iter.F (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
      (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ⋯ ⋯
⊢ Arrow.mk (iter.F.map (homOfLE ⋯)) =
    Arrow.mk (X :=
      obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) k₁ ⋯))
      (map (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (homOfLE ⋯))
have e_F₁ : (↑(sorry.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ≤ j
Tactic: rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc]
-- 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 : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
have dsimp : (ofCocone (colimit.cocone (inductiveSystem iter))).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry) =
  iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
Tactic: dsimp only [functor]
-- 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 : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
have rw : (inductiveSystem iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) =
  iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
Tactic: rw [ofCocone_obj_eq _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw : arrowMap (functor hj iter) i (Order.succ i) sorry sorry =
  Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw₁ : Arrow.mk (X := (iter i sorry).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry)) (Y :=
    Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) sorry))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) sorry))
    ((iter i sorry).mapObj (iter (Order.succ i) sorry) sorry sorry sorry sorry) =
  Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw₂ : arrowMap (F (iter (Order.succ i) sorry)) i (Order.succ i) sorry sorry =
  Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw₃ : arrowSucc (j := Order.succ i) (F (iter (Order.succ i) sorry)) i sorry =
  Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ :
  arrowSucc (j := Order.succ i) (F (iter (Order.succ i) ⋯)) i ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw₄ : Φ.toSuccArrow
    (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) sorry))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry)) =
  Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ :
  arrowSucc (j := Order.succ i) (F (iter (Order.succ i) ⋯)) i ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₄ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have rw₅ : Φ.toSuccArrow
    (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) sorry))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry)) =
  Φ.toSuccArrow
    (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) sorry))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ :
  arrowSucc (j := Order.succ i) (F (iter (Order.succ i) ⋯)) i ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₄ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₅ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have iter' : Φ.Iteration (Order.succ i)
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
rw :
  arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  Arrow.mk (X := (iter i ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)) (Y :=
      Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) (Order.succ i) ⋯))
      ((iter i ⋯).mapObj (iter (Order.succ i) ⋯) ⋯ ⋯ ⋯ ⋯) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ :
  arrowMap (F (iter (Order.succ i) ⋯)) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₃ :
  arrowSucc (j := Order.succ i) (F (iter (Order.succ i) ⋯)) i ⋯ =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₄ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₅ :
  Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)) =
    Φ.toSuccArrow
      (Functor.obj (C := (↑(Set.Iic (Order.succ i)) : Type u)) (F (iter (Order.succ i) ⋯))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
iter' : Φ.Iteration (Order.succ i)
⊢ arrowSucc (functor hj iter) i hi =
    Φ.toSuccArrow ((functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
have hk : i ≤ Order.succ i
Tactic: rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i)
        ((Order.IsSuccLimit.succ_lt_iff hj).2 hi), arrow_mk_mapObj,
      ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
      arrowSucc_eq, functor_obj _ _ _ 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
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
k : J
hk : k < i
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
have inl : ∀ (hij_1 : i < j), arrowMap (functor hj iter) k i sorry hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
Tactic: obtain hij | rfl := hij.lt_or_eq
-- 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 : i ≤ j
k : J
hk : k < i
inl : ∀ (hij_1 : i < j), arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
have inr : ∀ (hj : Order.IsSuccLimit i) (iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1) (hij : i ≤ i),
  arrowMap (functor hj iter) k i sorry hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
Tactic: obtain hij | rfl := hij.lt_or_eq
Cleared hypotheses: j, hj, iter, hij
-- 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
⊢ arrowMap (functor hj iter) k i ⋯ hij_1 = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk
have inl : arrowι (restrictionLT (iter i hij).F sorry) hi k hk = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk
Tactic: rw [arrowMap_functor _ _ _ _ _ hij, arrow_mk_mapObj,
        arrowMap_limit _ _ hi _ _ hk]