-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma contractible_mem_essImageDistTriang [EssSurj L] [HasZeroObject D]
    [HasZeroMorphisms D] [L.PreservesZeroMorphisms] (X : D) :
    contractibleTriangle X ∈ L.essImageDistTriang

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ contractibleTriangle X ≅ L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))

Tactic:
exact ((contractibleTriangleFunctor D).mapIso (L.objObjPreimageIso X)).symm ≪≫
  Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) L.mapZeroObject.symm (by simp) (by simp) (by simp)

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ contractibleTriangle X ∈ L.essImageDistTriang

Tactic:
refine ⟨contractibleTriangle (L.objPreimage X), ?_, contractible_distinguished _⟩

Result:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ contractibleTriangle X ≅ L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₂ ≫ L.mapZeroObject.symm.hom =
    (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₂).hom ≫
      (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₁ ≫
      (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₂).hom =
    (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₁).hom ≫
      (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₁

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{u_3, u_1} C
inst✝¹¹ : Category.{u_4, 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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₃ ≫
      (shiftFunctor D 1).map (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₁).hom =
    L.mapZeroObject.symm.hom ≫ (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₃

Tactic:
simp

Result:
no goals