-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_naturality (i : Δ ⟶ Δ') [Mono i] :
    mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ f.f Δ.len = f.f Δ'.len ≫ 0

Tactic:
rw [zero_comp, comp_zero]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = f.f Δ'.len ≫ K'.d Δ'.len Δ.len

Tactic:
rw [HomologicalComplex.Hom.comm]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len =
    f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0

Tactic:
split_ifs with h

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯

case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = f.f Δ'.len ≫ K'.d Δ'.len Δ.len

case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ f.f Δ.len = f.f Δ'.len ≫ 0

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
simp only [id_comp, eqToHom_refl, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i

Tactic:
unfold mapMono

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len =
    f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
subst h

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯