mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h

Tactic:
map_eq hj F τ i₁ i₂ _ h₂

Goal state after:
case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫ map hj F τ i₂ (Order.succ j) h₂₃ h

Tactic:
]

Goal state after:
case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
⊢ Φ.X₀ = Φ.X₀

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝ : i < Order.succ j
hi₁ : i ≤ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝ : i < Order.succ j
hi₁ : i ≤ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩) = Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩)) = Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ?inr✝⟩))

pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ i ≤ i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv = c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape 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 ⟨j, ⋯⟩))) hij) hi k hk

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape 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 ⟨j, ⋯⟩))) hij) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk ((ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv) = Arrow.mk (c.ι.app ⟨i, hi⟩)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk ((ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv) = Arrow.mk (c.ι.app ⟨i, hi⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
⊢ t ≫ ι' = t ≫ ι'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ⋯ =
    arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ?e_F.hi₂

pp: case e_F.hi₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ ↑(⋯.functor.obj ⟨k₂, h₂⟩) ≤ j

Tactic:
]

Goal state after:
case e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ⋯ =
    arrowMap iter.F ↑(⋯.functor.obj ⟨k₁, h₁⟩) ↑(⋯.functor.obj ⟨k₂, h₂⟩) ⋯ ?e_F.hi₂

case e_F.hi₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ ↑(⋯.functor.obj ⟨k₂, h₂⟩) ≤ j
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Φ.iter i₂).F i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Φ.iter i₂).F i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ : J
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ Φ.toSuccArrow ((iter (Order.succ i) ⋯).F.obj ⟨i, ⋯⟩) = Φ.toSuccArrow ((F ?iter').obj ⟨i, ?hk⟩)

pp: case iter'
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ Φ.Iteration ?m.192

pp: case hk
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ i ≤ ?m.192

pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ J

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) = (extendToSucc.objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE hi)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯ ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯ ≫ f)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowι (restrictionLT (iter i hij).F ⋯) hi k hk = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk

Tactic:
]

Goal state after:
case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
⊢ arrowι (restrictionLT (iter i hij).F ⋯) hi k hk = arrowι (restrictionLT (functor hj iter) hij✝) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
X' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
l : B i ⟶ functorObj f πX
hl₁ : f i ≫ l = (t ≫ eX.hom) ≫ ιFunctorObj f πX
hl₂ : l ≫ πFunctorObj f πX = b ≫ eS.hom
⊢ b ≫ eS.hom = b ≫ eS.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ (extendToSucc hj F τ).map (homOfLE hi) = (extendToSucc hj F τ).map (homOfLE hi)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Arrow.mk ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iter (Order.succ j)).F.obj ⟨j, ⋯⟩)
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iterationFunctor J).obj j)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
this : Arrow.mk ((Φ.iter (Order.succ j)).F.map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iter (Order.succ j)).F.obj ⟨j, ⋯⟩)
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE ⋯)) = Φ.toSuccArrow ((Φ.iterationFunctor J).obj j)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = arrowMap (iter l₂ ⋯).F l₁ l₂ pf✝ ⋯

Tactic:
]

Goal state after:
case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = arrowMap (iter l₂ ⋯).F l₁ l₂ pf✝ ⋯
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
]

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁹ : l₁ < i
pf✝⁸ : l₁ ∈ Set.Iic l₁
pf✝⁷ : l₂ < i
pf✝⁶ : l₂ ∈ Set.Iic l₂
pf✝⁵ : l₁ ≤ l₂
pf✝⁴ : l₁ ≤ l₁
pf✝³ : l₂ ≤ l₂
pf✝² : l₁ ∈ Set.Iic i
pf✝¹ : l₂ ∈ Set.Iic i
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter l₂ pf✝⁷).F l₁ l₂ pf✝⁵ pf✝³ = arrowMap (iter l₂ hl₂).F (↑⟨l₁, pf✝²⟩) l₂ pf✝ ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (⋯.functor.map f.unop).op))) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val

Tactic:
]

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val : F.obj (op j)
map_zero : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j✝ j'✝ : { x // x ∈ Set.Iio i }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map ((homOfLE ⋯).op ≫ (⋯.functor.map f.unop).op))) val =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val = val₀

Tactic:
]

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
⊢ (ConcreteCategory.hom (F.map ((homOfLE hij).op ≫ (homOfLE ⋯).op))) e.val = val₀
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val) =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val)

Tactic:
]

Goal state after: