-- 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:
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
⊢ ∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang

Tactic:
have := essSurj_mapArrow L W

Result:
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

Proof state:
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

Tactic:
obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle φ.hom

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
⊢ ∃ Z g h, 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
⊢ (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₃ ≫
      (shiftFunctor D 1).map (Arrow.leftFunc.mapIso e.symm).hom =
    (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 ≫
      (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₃

Tactic:
dsimp

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
⊢ (L.map h ≫ (L.commShiftIso 1).hom.app φ.left ≫ (shiftFunctor D 1).map e.hom.left) ≫
      (shiftFunctor D 1).map e.inv.left =
    𝟙 (L.obj Z) ≫ L.map h ≫ (L.commShiftIso 1).hom.app φ.left

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
⊢ 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)

Tactic:
refine Triangle.isoMk _ _ (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm)
  (Iso.refl _) e.inv.w.symm (by simp) ?_

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)).mor₃ ≫
      (shiftFunctor D 1).map (Arrow.leftFunc.mapIso e.symm).hom =
    (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 ≫
      (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₃

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
⊢ (L.map h ≫ (L.commShiftIso 1).hom.app φ.left ≫ (shiftFunctor D 1).map e.hom.left) ≫
      (shiftFunctor D 1).map e.inv.left =
    𝟙 (L.obj Z) ≫ L.map h ≫ (L.commShiftIso 1).hom.app φ.left

Tactic:
simp only [assoc, id_comp, ← Functor.map_comp, ← Arrow.comp_left, e.hom_inv_id, Arrow.id_left,
  Functor.mapArrow_obj, Arrow.mk_left, Functor.map_id, comp_id]

Result:
no goals