-- Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean
lemma hom_ext {Z : C} {φ₁ φ₂ : Y ⟶ Z} (h₀ : f ≫ φ₁ = f ≫ φ₂)
    (h : ∀ (γ : Cells c), γ.ι ≫ φ₁ = γ.ι ≫ φ₂) :
    φ₁ = φ₂

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₁ =
    ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₂

Tactic:
simpa using hj' k hk

Result:
no goals

Proof state:
case hs.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ ∀ (i : (c.attachCells j hj).ι),
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
      (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
intro i

Result:
case hs.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
i : (c.attachCells j hj).ι
⊢ (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Proof state:
case hm
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
hj : IsMin ⊥
⊢ c.incl.app ⊥ ≫ φ₁ = c.incl.app ⊥ ≫ φ₂

Tactic:
simpa [← cancel_epi c.isoBot.inv] using h₀

Result:
no goals

Proof state:
case hs
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.incl.app (Order.succ j) ≫ φ₁ = c.incl.app (Order.succ j) ≫ φ₂

Tactic:
apply (c.attachCells j hj).hom_ext

Result:
case hs.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₁ = c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₂

case hs.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ ∀ (i : (c.attachCells j hj).ι),
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
      (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
⊢ { pt := Y, ι := c.incl }.ι.app j ≫ φ₁ = { pt := Y, ι := c.incl }.ι.app j ≫ φ₂

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
⊢ c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂

Proof state:
case hl
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
⊢ c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂

Tactic:
exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
  (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)

Result:
no goals

Proof state:
case hs.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
⊢ c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₁ = c.F.map (homOfLE ⋯) ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
simpa using hj'

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
⊢ φ₁ = φ₂

Tactic:
refine c.isColimit.hom_ext (fun j ↦ ?_)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
⊢ { pt := Y, ι := c.incl }.ι.app j ≫ φ₁ = { pt := Y, ι := c.incl }.ι.app j ≫ φ₂