-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma distTriang_iff (T : Triangle D) :
    (T ∈ distTriang D) ↔ T ∈ 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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ distinguishedTriangles ↔ T ∈ L.essImageDistTriang

Tactic:
constructor

Result:
case mp
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ distinguishedTriangles → T ∈ L.essImageDistTriang

case mpr
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ L.essImageDistTriang → T ∈ distinguishedTriangles

Proof state:
case mpr
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ L.essImageDistTriang → T ∈ distinguishedTriangles

Tactic:
rintro ⟨T₀, e, hT₀⟩

Result:
case mpr.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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
T₀ : Triangle C
e : T ≅ L.mapTriangle.obj T₀
hT₀ : T₀ ∈ distinguishedTriangles
⊢ T ∈ distinguishedTriangles

Proof state:
case mpr.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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
T₀ : Triangle C
e : T ≅ L.mapTriangle.obj T₀
hT₀ : T₀ ∈ distinguishedTriangles
⊢ T ∈ distinguishedTriangles

Tactic:
exact isomorphic_distinguished _ (L.map_distinguished _ hT₀) _ e

Result:
no goals

Proof state:
case mp
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
⊢ T ∈ distinguishedTriangles → T ∈ L.essImageDistTriang

Tactic:
intro hT

Result:
case mp
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ T ∈ L.essImageDistTriang

Proof state:
case mp
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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
f : Arrow C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
⊢ T ∈ L.essImageDistTriang

Tactic:
obtain ⟨Z, g : f.right ⟶ Z, h : Z ⟶ f.left⟦(1 : ℤ)⟧, mem⟩ :=
  Pretriangulated.distinguished_cocone_triangle f.hom

Result:
case mp.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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
f : Arrow C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
Z : C
g : f.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj f.left
mem : Triangle.mk f.hom g h ∈ distinguishedTriangles
⊢ T ∈ L.essImageDistTriang

Proof state:
case mp.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 ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
f : Arrow C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
Z : C
g : f.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj f.left
mem : Triangle.mk f.hom g h ∈ distinguishedTriangles
⊢ T ∈ L.essImageDistTriang

Tactic:
exact ⟨_, (exists_iso_of_arrow_iso T _ hT (L.map_distinguished _ mem)
  (L.mapArrow.objObjPreimageIso T.mor₁).symm).choose, mem⟩

Result:
no goals