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

Goal state before:
pp: case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (if h₂ : i₃ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) =
    (if h₂ : i₂ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      if h₂ : i₃ < i₃ then (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else if h₁ : i₂ < i₃ then (objIso c i₂ h₁).hom ≫ c.ι.app ⟨i₂, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
·

Goal state after:
case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (if h₂ : i₃ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) =
    (if h₂ : i₂ < i₃ then (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else if h₁ : i₁ < i₃ then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      if h₂ : i₃ < i₃ then (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else if h₁ : i₂ < i₃ then (objIso c i₂ h₁).hom ≫ c.ι.app ⟨i₂, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else eqToHom ⋯
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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 ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), 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₂

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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 ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), 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₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case pos
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
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)

pp: case neg
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
hi : i ≤ Order.succ j
h₁ : ¬i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)

Tactic:
·

Goal state after:
case pos
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
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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₃

pp: case isSuccLimit.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
·

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case isSuccLimit.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
·

Goal state after:
case isSuccLimit.inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg
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
hi : i ≤ Order.succ j
h₁ : ¬i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)

Tactic:
·

Goal state after:
case neg
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
hi : i ≤ Order.succ j
h₁ : ¬i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), 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₃

pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), 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₃

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), 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₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inr
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₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃

Tactic:
·

Goal state after:
case inl.inr
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₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), 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₃

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ 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), 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₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case pos
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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

pp: case neg
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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

Tactic:
·

Goal state after:
case pos
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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inr
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₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃

Tactic:
·

Goal state after:
case inr
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₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f τ ≫ πFunctorObj f πY =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ πFunctorObj f πX ≫ Arrow.Hom.right τ

pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f τ ≫ πFunctorObj f πY =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ πFunctorObj f πX ≫ Arrow.Hom.right τ

Tactic:
·

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f τ ≫ πFunctorObj f πY =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ πFunctorObj f πX ≫ Arrow.Hom.right τ
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f τ ≫ πFunctorObj f πY =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ πFunctorObj f πX ≫ Arrow.Hom.right τ

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f τ ≫ πFunctorObj f πY =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ πFunctorObj f πX ≫ Arrow.Hom.right τ
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₀
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)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

pp: case h₁
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

Tactic:
·

Goal state after:
case h₀
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)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂),
    j₁ ≤ j₂ → iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
h : ¬j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

Tactic:
·

Goal state after:
case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂),
    j₁ ≤ j₂ → iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
h : ¬j₁ ≤ j₂
⊢ iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

Tactic:
·

Goal state after:
case h₁
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case neg
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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h

Tactic:
·

Goal state after:
case neg
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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂),
    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₂

pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
k₁ k₂ : J
h : k₁ ≤ k₂
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:
·

Goal state after:
case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂),
    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₂