Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃'
v₁₂' : X₂' ⟶ Z₁₂'
w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁'
h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distinguishedTriangles
v₂₃' : X₃' ⟶ Z₂₃'
w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂'
h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distinguishedTriangles
v₁₃' : X₃' ⟶ Z₁₃'
w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁'
h₁₃' : Triangle.mk u₁₃' v₁₃' w₁₃' ∈ distinguishedTriangles
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
⊢ Octahedron comm h₁₂ h₂₃ h₁₃

Tactic:
by
  let iso₁₂ := isoTriangleOfIso₁₂ _ _ h₁₂ h₁₂' e₁ e₂ comm₁₂
  let iso₂₃ := isoTriangleOfIso₁₂ _ _ h₂₃ h₂₃' e₂ e₃ comm₂₃
  let iso₁₃ := isoTriangleOfIso₁₂ _ _ h₁₃ h₁₃' e₁ e₃ (by
    dsimp; rw [← comm, assoc, ← comm', ← reassoc_of% comm₁₂, comm₂₃])
  have eq₁₂ := iso₁₂.hom.comm₂
  have eq₁₂' := iso₁₂.hom.comm₃
  have eq₁₃ := iso₁₃.hom.comm₂
  have eq₁₃' := iso₁₃.hom.comm₃
  have eq₂₃ := iso₂₃.hom.comm₂
  have eq₂₃' := iso₂₃.hom.comm₃
  have rel₁₂ := H.triangleMorphism₁.comm₂
  have rel₁₃ := H.triangleMorphism₁.comm₃
  have rel₂₂ := H.triangleMorphism₂.comm₂
  have rel₂₃ := H.triangleMorphism₂.comm₃
  dsimp [iso₁₂, iso₂₃, iso₁₃] at eq₁₂ eq₁₂' eq₁₃ eq₁₃' eq₂₃ eq₂₃' rel₁₂ rel₁₃ rel₂₂ rel₂₃
  rw [Functor.map_id, comp_id] at rel₁₃
  rw [id_comp] at rel₂₂
  refine ⟨iso₁₂.hom.hom₃ ≫ H.m₁ ≫ iso₁₃.inv.hom₃,
    iso₁₃.hom.hom₃ ≫ H.m₃ ≫ iso₂₃.inv.hom₃, ?_, ?_, ?_, ?_, ?_⟩
  · rw [reassoc_of% eq₁₂, ← cancel_mono iso₁₃.hom.hom₃, assoc, assoc, assoc, assoc,
      iso₁₃.inv_hom_id_triangle_hom₃, eq₁₃, reassoc_of% comm₂₃, ← rel₁₂]
    dsimp
    rw [comp_id]
  · rw [← cancel_mono (e₁.hom⟦(1 : ℤ)⟧'), eq₁₂', assoc, assoc, assoc, eq₁₃',
      iso₁₃.inv_hom_id_triangle_hom₃_assoc, ← rel₁₃]
  · rw [reassoc_of% eq₁₃, reassoc_of% rel₂₂, ← cancel_mono iso₂₃.hom.hom₃, assoc, assoc,
      iso₂₃.inv_hom_id_triangle_hom₃, eq₂₃]
    dsimp
    rw [comp_id]
  · rw [← cancel_mono (e₂.hom⟦(1 : ℤ)⟧'), assoc, assoc, assoc, assoc, eq₂₃',
      iso₂₃.inv_hom_id_triangle_hom₃_assoc, ← rel₂₃, ← Functor.map_comp, comm₁₂,
      Functor.map_comp, reassoc_of% eq₁₃']
  · refine isomorphic_distinguished _ H.mem _ ?_
    refine Triangle.isoMk _ _ (Triangle.π₃.mapIso iso₁₂) (Triangle.π₃.mapIso iso₁₃)
      (Triangle.π₃.mapIso iso₂₃) (by simp) (by simp) ?_
    dsimp
    rw [assoc, ← Functor.map_comp, eq₁₂, Functor.map_comp, reassoc_of% eq₂₃']

Goal state after: