awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc :
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯)
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j) (h : k₂ ≤ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
neg : arrowMap iter₁.F (Order.succ j) (Order.succ j) h₁₂ h₂ = arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
neg₁ :
  Arrow.mk (𝟙 (iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h₂))) =
    arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
neg₂ :
  Eq (α := Arrow.{v, u} C)
    (Arrow.mk (𝟙 (iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h₂))))
    (Arrow.mk (𝟙 (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h₂))))
neg₃ :
  Eq (α := Arrow.{v, u} C)
    (Arrow.mk (𝟙 (Φ.succ (iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯)))))
    (Arrow.mk (𝟙 (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h₂))))
neg₄ :
  Eq (α := Arrow.{v, u} C)
    (Arrow.mk (𝟙 (Φ.succ (iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯)))))
    (Arrow.mk (𝟙 (Φ.succ (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯)))))
⊢ MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
have neg₅ : Eq (α := Arrow.{v, u} C)
  (Arrow.mk (𝟙 (Φ.succ (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry)))))
  (Arrow.mk (𝟙 (Φ.succ (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry)))))
Tactic: rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
⊢ iter₁.F = iter₂.F
have isSuccLimit : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
Tactic: refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
have isSuccLimit : ∀ (this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃) (h₄ : ¬k₂ < j),
  MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
Tactic: wlog h₄ : k₂ < j generalizing k₁ k₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
isSuccLimit :
  ∀ (this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃)
    (h₄ : ¬k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
have wlog : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
Tactic: wlog h₄ : k₂ < j generalizing k₁ k₂
Cleared hypotheses: k₁, k₂, h₁₂, h₃
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
have this : (iter₁.trunc sorry).F = (iter₂.trunc sorry).F
Tactic: have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
have isSuccLimit : ∀ (h₁₂ : k₁ ≤ j) (h₃ : j ≤ j) (h₄ : ¬j < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
Tactic: obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
Cleared hypotheses: k₂, h₁₂, h₃, h₄
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
have this₁ : restrictionLT iter₁.F sorry = restrictionLT iter₂.F sorry
Tactic: have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
have pos : ∀ (h₅ : k₁ < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
Tactic: by_cases h₅ : k₁ < j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
pos : ∀ (h₅ : k₁ < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
have neg : ∀ (h₅ : ¬k₁ < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
Tactic: by_cases h₅ : k₁ < j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : k₁ < j
⊢ arrowMap iter₁.F k₁ j h₁₂ h₃ = arrowMap iter₂.F k₁ j h₁₂ h₃
have pos : arrowι (restrictionLT iter₁.F h₃) h₁ k₁ h₅ = arrowι (restrictionLT iter₂.F h₃) h₁ k₁ h₅
Tactic: simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
have neg : ∀ (h₁ : Order.IsSuccLimit k₁) (h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F)
  (iter₁ iter₂ : Φ.Iteration k₁)
  (this : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁) (h₄ : k₂ < k₁), MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃)
  (h₁₂ h₃ : k₁ ≤ k₁) (h₄ : ¬k₁ < k₁) (this : restrictionLT iter₁.F sorry = restrictionLT iter₂.F sorry) (h₅ : ¬k₁ < k₁),
  MapEq iter₁.F iter₂.F k₁ k₁ h₁₂ h₃
Tactic: obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
Cleared hypotheses: j, h₁, h₂, iter₁, iter₂, this_1, h₁₂, h₃, h₄, this, h₅
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j k₁ : J
h₁ : Order.IsSuccLimit k₁
h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration k₁
this_1 : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁) (h₄ : k₂ < k₁), MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃
h₁₂ h₃ : k₁ ≤ k₁
h₄ : ¬k₁ < k₁
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < k₁
⊢ MapEq iter₁.F iter₂.F k₁ k₁ h₁₂ h₃
have neg : iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃) =
  iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃)
Tactic: apply mapEq_refl
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
have isMin : ∀ (j : J) (h : IsMin j) (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
Tactic: induction j using SuccOrder.limitRecOn with
    | isMin j h =>
      obtain rfl := h.eq_bot
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      obtain rfl : k₂ = ⊥ := by simpa using h₂
      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
      apply mapEq_refl _ _ (by simp only [obj_bot])
    | succ j hj₁ hj₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      have h₀ := Order.le_succ j
      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
      dsimp at hj₂ hsucc
      wlog h : k₂ ≤ j generalizing k₁ k₂
      · obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
    | isSuccLimit j h₁ h₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
isMin : ∀ (j : J) (h : IsMin j) (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
have succ : ∀ (j : J) (hj₁ : ¬IsMax j) (hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F)
  (iter₁ iter₂ : Φ.Iteration (Order.succ j)), iter₁.F = iter₂.F
Tactic: induction j using SuccOrder.limitRecOn with
    | isMin j h =>
      obtain rfl := h.eq_bot
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      obtain rfl : k₂ = ⊥ := by simpa using h₂
      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
      apply mapEq_refl _ _ (by simp only [obj_bot])
    | succ j hj₁ hj₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      have h₀ := Order.le_succ j
      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
      dsimp at hj₂ hsucc
      wlog h : k₂ ≤ j generalizing k₁ k₂
      · obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
    | isSuccLimit j h₁ h₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
isMin : ∀ (j : J) (h : IsMin j) (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
succ :
  ∀ (j : J) (hj₁ : ¬IsMax j) (hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F)
    (iter₁ iter₂ : Φ.Iteration (Order.succ j)), iter₁.F = iter₂.F
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
have isSuccLimit : ∀ (j : J) (h₁ : Order.IsSuccLimit j) (h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F)
  (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
Tactic: induction j using SuccOrder.limitRecOn with
    | isMin j h =>
      obtain rfl := h.eq_bot
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      obtain rfl : k₂ = ⊥ := by simpa using h₂
      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
      apply mapEq_refl _ _ (by simp only [obj_bot])
    | succ j hj₁ hj₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      have h₀ := Order.le_succ j
      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
      dsimp at hj₂ hsucc
      wlog h : k₂ ≤ j generalizing k₁ k₂
      · obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
    | isSuccLimit j h₁ h₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
have inr : ∀
  (this :
    ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
      iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
        iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂))
  (h : ¬j₁ ≤ j₂),
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
Tactic: wlog h : j₁ ≤ j₂ generalizing j₁ j₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
inr :
  ∀
    (this :
      ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
        iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
          iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂))
    (h : ¬j₁ ≤ j₂),
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
have wlog : ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
Tactic: wlog h : j₁ ≤ j₂ generalizing j₁ j₂
Cleared hypotheses: j₁, j₂, iter₁, iter₂, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
have rw : (iter₂.trunc h).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
  iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
Tactic: rw [Subsingleton.elim iter₁ (iter₂.trunc h)]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
have inr : ∀
  (this :
    ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
      arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂)
  (hj : ¬j₁ ≤ j₂), arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
Tactic: wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
inr :
  ∀
    (this :
      ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
        arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂)
    (hj : ¬j₁ ≤ j₂), arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
have wlog : ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
  arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
Tactic: wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
Cleared hypotheses: j₁, j₂, iter₁, iter₂, h₁, h₂