-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
@[reassoc (attr := simp)]
lemma πTruncGE_naturality :
    K.πTruncGE e ≫ truncGEMap φ e = φ ≫ L.πTruncGE e

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.πTruncGE e ≫ truncGEMap φ e = φ ≫ L.πTruncGE e

Tactic:
apply (e.homEquiv _ _).injective

Result:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ (e.homEquiv K (L.truncGE' e)) (K.πTruncGE e ≫ truncGEMap φ e) = (e.homEquiv K (L.truncGE' e)) (φ ≫ L.πTruncGE e)

Proof state:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ (e.homEquiv K (L.truncGE' e)) (K.πTruncGE e ≫ truncGEMap φ e) = (e.homEquiv K (L.truncGE' e)) (φ ≫ L.πTruncGE e)

Tactic:
ext1

Result:
case a.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ ↑((e.homEquiv K (L.truncGE' e)) (K.πTruncGE e ≫ truncGEMap φ e)) = ↑((e.homEquiv K (L.truncGE' e)) (φ ≫ L.πTruncGE e))

Proof state:
case a.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ e.homRestrict (e.liftExtend (K.restrictionToTruncGE' e) ⋯ ≫ extendMap (truncGE'Map φ e) e) =
    e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯)

Tactic:
rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
  e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]

Result:
no goals

Proof state:
case a.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ ↑((e.homEquiv K (L.truncGE' e)) (K.πTruncGE e ≫ truncGEMap φ e)) = ↑((e.homEquiv K (L.truncGE' e)) (φ ≫ L.πTruncGE e))

Tactic:
dsimp [truncGEMap, πTruncGE]

Result:
case a.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ e.homRestrict (e.liftExtend (K.restrictionToTruncGE' e) ⋯ ≫ extendMap (truncGE'Map φ e) e) =
    e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯)