-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma ext_succ {F G : ComposableArrows C (n + 1)} (h₀ : F.obj' 0 = G.obj' 0)
    (h : F.δ₀ = G.δ₀) (w : F.map' 0 1 = eqToHom h₀ ≫ G.map' 0 1 ≫
      eqToHom (Functor.congr_obj h.symm 0)) : F = G

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ i < n + 1

Tactic:
valid

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i < n + 1 + 1
⊢ F.obj ⟨i, hi⟩ = G.obj ⟨i, hi⟩

Tactic:
rcases i with - | i

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
hi : 0 < n + 1 + 1
⊢ F.obj ⟨0, hi⟩ = G.obj ⟨0, hi⟩

case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ F.obj ⟨i + 1, hi⟩ = G.obj ⟨i + 1, hi⟩

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
hi : 0 < n + 1 + 1
⊢ F.obj ⟨0, hi⟩ = G.obj ⟨0, hi⟩

Tactic:
exact h₀

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
⊢ ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i

Tactic:
intro ⟨i, hi⟩

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i < n + 1 + 1
⊢ F.obj ⟨i, hi⟩ = G.obj ⟨i, hi⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F.map' 0 1 ⋯ ⋯ ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 ⋯ ⋯

Tactic:
rw [w]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯) ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 ⋯ ⋯

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ F.obj ⟨i + 1, hi⟩ = G.obj ⟨i + 1, hi⟩

Tactic:
exact Functor.congr_obj h ⟨i, by valid⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F = G

Tactic:
exact Functor.ext_of_iso (isoMkSucc (eqToIso h₀) (eqToIso h) (by
    rw [w]
    dsimp [app']
    rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id])) this
  (by rintro ⟨_|_, hi⟩ <;> simp)

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ ∀ (X : Fin (n + 1 + 1)), (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app X = eqToHom ⋯

Tactic:
rintro ⟨_|_, hi⟩ <;> simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯) ≫ (eqToHom h).app 0 = eqToHom h₀ ≫ G.map (homOfLE ⋯)

Tactic:
rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯) ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 ⋯ ⋯

Tactic:
dsimp [app']

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 ⋯ ⋯ = eqToHom h₀ ≫ G.map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯) ≫ (eqToHom h).app 0 = eqToHom h₀ ≫ G.map (homOfLE ⋯)