-- Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
lemma mem_distTriang_iff (T : Triangle (DerivedCategory C)) :
    (T ∈ distTriang (DerivedCategory C)) ↔ ∃ (X Y : CochainComplex C ℤ) (f : X ⟶ Y),
      Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ T ∈ distinguishedTriangles ↔ ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ T ∈ distinguishedTriangles → ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ (∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))) → T ∈ distinguishedTriangles

Proof state:
case mpr.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
X Y : CochainComplex C ℤ
f : X ⟶ Y
e : T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)
⊢ T ∈ distinguishedTriangles

Tactic:
refine isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
  (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
  (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)

Result:
case mpr.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
X Y : CochainComplex C ℤ
f : X ⟶ Y
e : T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingCone.triangle f) ∈
    distinguishedTriangles

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ T ∈ distinguishedTriangles → ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Tactic:
rintro ⟨T', e, ⟨X, Y, f, ⟨e'⟩⟩⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
T' : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T ≅ Qh.mapTriangle.obj T'
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ (∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))) → T ∈ distinguishedTriangles

Tactic:
rintro ⟨X, Y, f, ⟨e⟩⟩

Result:
case mpr.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
X Y : CochainComplex C ℤ
f : X ⟶ Y
e : T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)
⊢ T ∈ distinguishedTriangles

Proof state:
case mp.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
T' : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T ≅ Qh.mapTriangle.obj T'
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)

Tactic:
exact e ≪≫ Qh.mapTriangle.mapIso e' ≪≫
  (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).symm.app _ ≪≫
  (Functor.mapTriangleIso (quotientCompQhIso C)).app _

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
X Y : CochainComplex C ℤ
f : X ⟶ Y
e : T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingCone.triangle f) ∈
    distinguishedTriangles

Tactic:
exact ⟨_, _, f, ⟨Iso.refl _⟩⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
T' : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T ≅ Qh.mapTriangle.obj T'
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Tactic:
refine ⟨_, _, f, ⟨?_⟩⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
T' : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T ≅ Qh.mapTriangle.obj T'
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)