-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
refine_1 : e₁.hom.hom₂ ≫ L.map T₁'.mor₂ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₁ : e₁.hom.hom₂ ≫ φ.hom₂ ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₂ : e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₃ : e₁.hom.hom₂ ≫ e₁.inv.hom₂ ≫ (b ≫ e₂.hom.hom₂) ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
have refine_1₄ : e₁.hom.hom₂ ≫ e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂ ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
      Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
      Iso.hom_inv_id_triangle_hom₃, comp_id]