awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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) ⊥ ⊥
isMin : ∀ (h₁₂ : LE.le.{w} (α := J) ⊥ ⊥), MapEq iter₁.F iter₂.F ⊥ ⊥ h₁₂ h₂
⊢ MapEq iter₁.F iter₂.F k₁ ⊥ h₁₂ h₂

Tactic:
obtain rfl : k₁ = ⊥ := by simpa using h₁₂

Premises used: rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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) Φ ⊥
h₂ h₁₂ : LE.le.{w} (α := J) ⊥ ⊥
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iic ⊥) x) ⊥ h₂) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iic ⊥) x) ⊥ h₂)

Tactic:
simp only [obj_bot]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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) Φ ⊥
h₂ h₁₂ : LE.le.{w} (α := J) ⊥ ⊥
⊢ MapEq iter₁.F iter₂.F ⊥ ⊥ h₁₂ h₂

Tactic:
apply mapEq_refl _ _ (by simp only [obj_bot])

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_refl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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

Tactic:
ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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)
succ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
⊢ iter₁.F = iter₂.F

Tactic:
refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ j ≤ Order.succ j

Tactic:
have h₀ := Order.le_succ j
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ (iter₁.trunc h₀).F = (iter₂.trunc h₀).F

Tactic:
replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ j ∈ Set.Iic j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ (iter₁.trunc h₀).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) =
    (iter₂.trunc h₀).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)

Tactic:
have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₂
wlog : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j) (h : k₂ ≤ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
wlog h : k₂ ≤ j generalizing k₁ k₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₂
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₂
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
obtain h₂ | rfl := h₂.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₂_1 : 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
h₂ : k₂ < Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂_1

Tactic:
this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)

Premises used: Iff.mp, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₂_1 : 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
h₂ : k₂ < Order.succ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂_1

Tactic:
exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)

Premises used: Iff.mp, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₂
neg : ∀ (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₂

Tactic:
by_cases h' : k₁ ≤ j
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ j ≤ j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
pos : MapEq iter₁.F iter₂.F j (Order.succ j) h₀ h₂
⊢ MapEq iter₁.F iter₂.F k₁ (Order.succ j) h₁₂ h₂

Tactic:
apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_trans
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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 j (Order.succ j) h₀ h₂

Tactic:
simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]

Premises used: Order.lt_succ_of_not_isMax, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq, CategoryTheory.SmallObject.SuccStruct.arrowSucc_def
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ j < k₁

Tactic:
simp only [not_le] at h'

Premises used: not_le
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₁
⊢ k₁ = Order.succ j

Tactic:
le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')

Premises used: Iff.mpr, Order.succ_le_iff_of_not_isMax, le_antisymm
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₁
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₂
⊢ MapEq iter₁.F iter₂.F k₁ (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')

Premises used: Iff.mpr, Order.succ, Order.succ_le_iff_of_not_isMax, le_antisymm, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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 ⋯)))))
neg₅ 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₂

Tactic:
rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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 ⋯)
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ Order.succ j
h : k₂ ≤ j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap_restrictionLE, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq, Order.le_succ
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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

Tactic:
ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
isSuccLimit : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
⊢ iter₁.F = iter₂.F

Tactic:
refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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₃
wlog : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
wlog h₄ : k₂ < j generalizing k₁ k₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ (iter₁.trunc ⋯).F = (iter₂.trunc ⋯).F

Tactic:
have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
this : restrictionLE iter₁.F ⋯ = restrictionLE iter₂.F ⋯
⊢ k₂ ≤ k₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
this : restrictionLE iter₁.F ⋯ = restrictionLE iter₂.F ⋯
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]

Premises used: LT.lt.le, CategoryTheory.SmallObject.SuccStruct.arrowMap_restrictionLE, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
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
⊢ j ≤ k₂

Tactic:
simpa using h₄