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
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ F.map (homOfLE ⋯) = eqToHom ⋯ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯
have rw : F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) = eqToHom sorry ≫ G.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ eqToHom sorry
Tactic: rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
⊢ F = G
have h₁ : ∀ ⦃X Y : (↑(Set.Iic x) : Type w)⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)
Tactic: apply Arrow.functor_ext
-- 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₁ = iter₂
have suffices : iter₁.F = iter₂.F
Tactic: suffices iter₁.F = iter₂.F by aesop
-- 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 revert : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
Tactic: revert iter₁ iter₂
Cleared hypotheses: iter₁, iter₂
-- 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 : IsMin j
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
have isMin : ∀ (h : IsMin.{w} (α := J) ⊥) (iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥), iter₁.F = iter₂.F
Tactic: obtain rfl := h.eq_bot
Cleared hypotheses: j, 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
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
⊢ iter₁.F = iter₂.F
have isMin : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ ⊥), 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 : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ ⊥
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have isMin : ∀ (h₁₂ : k₁ ≤ ⊥) (h₂ : LE.le.{w} (α := J) ⊥ ⊥), MapEq iter₁.F iter₂.F k₁ ⊥ h₁₂ h₂
Tactic: obtain rfl : k₂ = ⊥ := by simpa using h₂
Cleared hypotheses: 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 : J
h : IsMin.{w} (α := J) ⊥
iter₁ iter₂ : Iteration.{w, v, u} (J := J) Φ ⊥
k₁ : J
h₁₂ : k₁ ≤ ⊥
h₂ : LE.le.{w} (α := J) ⊥ ⊥
⊢ MapEq iter₁.F iter₂.F k₁ ⊥ h₁₂ h₂
have isMin : ∀ (h₁₂ : LE.le.{w} (α := J) ⊥ ⊥), MapEq iter₁.F iter₂.F ⊥ ⊥ h₁₂ h₂
Tactic: obtain rfl : k₁ = ⊥ := by simpa using h₁₂
Cleared hypotheses: k₁, 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
hj₁ : ¬IsMax j
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
⊢ iter₁.F = iter₂.F
have succ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ 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 (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
hj₁ : ¬IsMax j
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have h₀ : j ≤ Order.succ j
Tactic: have h₀ := Order.le_succ j
-- 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
hj₁ : ¬IsMax j
hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have hj₃ : (iter₁.trunc h₀).F = (iter₂.trunc h₀).F
Tactic: replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
Cleared hypotheses: hj₂
-- 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h₀ : j ≤ Order.succ j
hj₂ : (iter₁.trunc h₀).F = (iter₂.trunc h₀).F
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have hsucc : (iter₁.trunc h₀).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry) =
  (iter₂.trunc h₀).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)
Tactic: have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
-- 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)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ 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 ⋯)
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have succ : ∀ (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 : ¬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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ 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 ⋯)
succ :
  ∀ (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 : ¬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₂ ≤ Order.succ 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 (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)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ 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 : ¬k₂ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have succ : ∀ (h₂_1 : k₂ < Order.succ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
Tactic: obtain h₂ | rfl := h₂.lt_or_eq
-- 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)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ 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 : ¬k₂ ≤ j
succ : ∀ (h₂_1 : k₂ < Order.succ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
have succ₁ : ∀ (h₁₂ : k₁ ≤ Order.succ j) (h₂ : Order.succ j ≤ Order.succ j) (h : ¬Order.succ j ≤ j),
  MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
Tactic: obtain h₂ | rfl := h₂.lt_or_eq
Cleared hypotheses: k₂, h₁₂, 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : 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₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
have pos : ∀ (h' : k₁ ≤ j), MapEq iter₁.F iter₂.F k₁ (Order.succ 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : 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₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
pos : ∀ (h' : k₁ ≤ j), MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
have neg : ∀ (h' : ¬k₁ ≤ j), MapEq iter₁.F iter₂.F k₁ (Order.succ 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : 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₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
have pos : MapEq iter₁.F iter₂.F j (Order.succ j) h₀ h₂
Tactic: apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
-- 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : 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₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : ¬k₁ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
have h'₁ : j < k₁
Tactic: simp only [not_le] at h'
Cleared hypotheses: 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
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
k₁ : 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₁₂ : k₁ ≤ Order.succ j
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h' : j < k₁
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂
have neg : ∀ (h₁₂ : Order.succ j ≤ Order.succ j) (h' : j < Order.succ j),
  MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
Tactic: obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
Cleared hypotheses: 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
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
⊢ MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
have neg : arrowMap iter₁.F (Order.succ j) (Order.succ j) h₁₂ h₂ = arrowMap iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
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
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₂
⊢ MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
have 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₂
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
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₂
⊢ MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂
have 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₂))))
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
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₂))))
⊢ 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 (𝟙 (iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h₂))))
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
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₂))))
⊢ 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]