-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem hσ'_naturality (q : ℕ) (n m : ℕ) (hnm : c.Rel m n) {X Y : SimplicialObject C} (f : X ⟶ Y) :
    f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ f.app (op ⦋n⦌) ≫ hσ q n = hσ q n ≫ f.app (op ⦋n + 1⦌)

Tactic:
unfold hσ

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else (-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) =
    (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject C
f : X ⟶ Y
h : n + 1 = m
⊢ f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)

Tactic:
subst h

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ f.app (op ⦋n + 1⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else (-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) =
    (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Tactic:
split_ifs

Result:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
h✝ : n < q
⊢ f.app (op ⦋n⦌) ≫ 0 = 0 ≫ f.app (op ⦋n + 1⦌)

case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
h✝ : ¬n < q
⊢ f.app (op ⦋n⦌) ≫ ((-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) = ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Proof state:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
h✝ : n < q
⊢ f.app (op ⦋n⦌) ≫ 0 = 0 ≫ f.app (op ⦋n + 1⦌)

Tactic:
rw [zero_comp, comp_zero]

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
h✝ : ¬n < q
⊢ f.app (op ⦋n⦌) ≫ ((-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) = ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ f.app (op ⦋n + 1⦌)

Tactic:
simp only [hσ', eqToHom_refl, comp_id]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : c.Rel (n + 1) n
⊢ f.app (op ⦋n⦌) ≫ hσ q n = hσ q n ≫ f.app (op ⦋n + 1⦌)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)

Tactic:
have h : n + 1 = m := hnm

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject C
f : X ⟶ Y
h : n + 1 = m
⊢ f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)