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
⊢ 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)) ⊥ ⋯) =
    Φ.X₀
have rw : iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) ⊥ sorry) = Φ.X₀
Tactic: rw [extendToSucc_obj_eq _ _ _ _ bot_le, obj_bot]
-- 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
rw : iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) ⊥ ⋯) = Φ.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)) ⊥ ⋯) =
    Φ.X₀
have rw₁ : Φ.X₀ = Φ.X₀
Tactic: rw [extendToSucc_obj_eq _ _ _ _ bot_le, obj_bot]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (hypothesis)
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₁ : i < Order.succ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i hi₁ =
    Φ.toSuccArrow
      (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)) i ⋯))
have hi₂ : i ≤ j
Tactic: rw [Order.lt_succ_iff_of_not_isMax hj] at 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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁_1 : i < Order.succ j
hi₁ : i ≤ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl : ∀ (hi₁ : i < j),
  arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i sorry))
Tactic: obtain hi₁ | rfl := hi₁.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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁_1 : i < Order.succ j
hi₁ : i ≤ j
inl :
  ∀ (hi₁ : i < j),
    arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
        hi₁_1 =
      Φ.toSuccArrow
        (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)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inr : ∀ (hj : ¬IsMax i) (iter : Φ.Iteration i) (hi₁ : i < Order.succ i) (hi₁_2 : i ≤ i),
  arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry)))) i hi₁ =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry))
Tactic: obtain hi₁ | rfl := hi₁.lt_or_eq
Cleared hypotheses: j, hj, iter, hi₁_1, 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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl : arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)))) i
    (Order.succ i) sorry sorry =
  Φ.toSuccArrow
    (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)) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
-- 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₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
inl :
  arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl₁ : arrowMap iter.F i (Order.succ i) sorry sorry =
  Φ.toSuccArrow
    (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)) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
-- 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₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
inl :
  arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl₂ : arrowSucc iter.F i hi₁ =
  Φ.toSuccArrow
    (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)) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
-- 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₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
inl :
  arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₂ :
  arrowSucc iter.F i hi₁ =
    Φ.toSuccArrow
      (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)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl₃ : Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) =
  Φ.toSuccArrow
    (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)) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
-- 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₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
inl :
  arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₂ :
  arrowSucc iter.F i hi₁ =
    Φ.toSuccArrow
      (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)) i ⋯))
inl₃ :
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) =
    Φ.toSuccArrow
      (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)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (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)) i ⋯))
have inl₄ : Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) =
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
-- 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
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁_1 : i < Order.succ i
hi₁ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
have inr : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))
    (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))) =
  Φ.toSuccArrow
    (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
      (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry))
Tactic: rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]
-- 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
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁_1 : i < Order.succ i
hi₁ : i ≤ i
inr :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
have inr₁ : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))
    (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))) =
  Arrow.mk (X :=
    obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
      (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry))
    (Φ.toSucc
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i sorry)))
Tactic: rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]
-- 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
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁_1 : i < Order.succ i
hi₁ : i ≤ i
inr :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
inr₁ :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Arrow.mk (X :=
      obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
      (Φ.toSucc
        (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
          (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
have inr₂ : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))
    (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))) =
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry))
    (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i sorry)))
Tactic: rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (hypothesis)
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
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) k i ⋯
      hij =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk
have hij' : i ≤ j
Tactic: have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 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 : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) k i ⋯
      hij =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk
have rw : arrowι (restrictionLT iter.F hij') hi k hk =
  arrowι
    (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))))
      hij)
    hi k hk
Tactic: rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk]
-- 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
⊢ arrowι (restrictionLT iter.F hij') hi k hk =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk
have e_F : restrictionLT iter.F hij' =
  restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)))) hij
Tactic: congr 1