-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma distinguished_cocone_triangle {X Y : D} (f : X ⟶ Y) :
    ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧),
      Triangle.mk f g h ∈ L.essImageDistTriang

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_4, u_1} C
inst✝⁹ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : (𝟭 C).obj φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang

Tactic:
refine ⟨L.obj Z, e.inv.right ≫ L.map g,
  L.map h ≫ (L.commShiftIso (1 : ℤ)).hom.app _ ≫ e.hom.left⟦(1 : ℤ)⟧', _, ?_, H⟩

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_4, u_1} C
inst✝⁹ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : (𝟭 C).obj φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ Triangle.mk f (e.inv.right ≫ L.map g)
      (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left) ≅
    L.mapTriangle.obj (Triangle.mk φ.hom g h)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_4, u_1} C
inst✝⁹ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : (𝟭 C).obj φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ (Triangle.mk f (e.inv.right ≫ L.map g)
          (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left)).mor₂ ≫
      (Iso.refl
          (Triangle.mk f (e.inv.right ≫ L.map g)
              (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left)).obj₃).hom =
    (Arrow.rightFunc.mapIso e.symm).hom ≫ (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_4, u_1} C
inst✝⁹ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang

Tactic:
obtain ⟨φ, ⟨e⟩⟩ : ∃ (φ : Arrow C), Nonempty (L.mapArrow.obj φ ≅ Arrow.mk f) :=
  ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_4, u_1} C
inst✝⁹ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang