Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫ T₂.mor₃
⊢ T₁.mor₂ ≫ γ.hom₃ = b ≫ T₂.mor₂

pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫ T₂.mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = γ.hom₃ ≫ T₂.mor₃

Tactic:
· simpa only [triangleCategory_comp, Functor.mapTriangle_obj, triangle_obj₁, triangle_obj₂,
      triangle_obj₃, triangle_mor₁, triangle_mor₂, TriangleMorphism.comp_hom₃, Triangle.mk_obj₃,
      trianglehMapOfHomotopy_hom₃, TriangleMorphism.comm₂_assoc, Triangle.mk_obj₂,
      Triangle.mk_mor₂, assoc, Iso.hom_inv_id_triangle_hom₂, comp_id,
      Iso.hom_inv_id_triangle_hom₂_assoc, γ] using comm₂

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫ T₂.mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = γ.hom₃ ≫ T₂.mor₃