-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc (attr := simp)]
lemma mappingConeCompTriangleh_comm₁ :
    (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient _ _).map (mappingConeCompHomotopyEquiv f g).hom =
    (HomotopyCategory.quotient _ _).map (mappingCone.inr _)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁)

Tactic:
rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv
    (mappingConeCompHomotopyEquiv f g)).inv, assoc]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁) ≫
      (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv

Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, ← Functor.map_comp,
  mappingConeCompHomotopyEquiv_hom_inv_id, comp_id,
  mappingConeCompHomotopyEquiv_comm₁ f g,
  mappingConeCompTriangle_mor₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁) ≫
      (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv

Tactic:
dsimp [mappingConeCompTriangleh]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv