-- Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
lemma distinguished_iff_iso_trianglehOfDegreewiseSplit
    (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))) :
    (T ∈ distTriang _) ↔ ∃ (S : ShortComplex (CochainComplex C ℤ))
      (σ : ∀ n, (S.map (HomologicalComplex.eval C _ n)).Splitting),
      Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles → ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
intro hT

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
⊢ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Proof state:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T ∈ distinguishedTriangles

Tactic:
rw [rotate_distinguished_triangle, rotate_distinguished_triangle]

Result:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T.rotate.rotate ∈ distinguishedTriangles

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
⊢ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := inv_rot_of_distTriang _ hT

Result:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T.invRotate ≅ CochainComplex.mappingCone.triangleh φ
⊢ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Proof state:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ) ∈ distinguishedTriangles

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

Result:
no goals

Proof state:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T.rotate.rotate ∈ distinguishedTriangles

Tactic:
refine isomorphic_distinguished _ ?_ _
  ((rotate _ ⋙ rotate _).mapIso e ≪≫
    CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso S σ)

Result:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ CochainComplex.mappingCone.triangleh (CochainComplex.homOfDegreewiseSplit S σ) ∈ distinguishedTriangles

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles ↔ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles → ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

case mpr
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ (∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) → T ∈ distinguishedTriangles

Proof state:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T.invRotate ≅ CochainComplex.mappingCone.triangleh φ
⊢ ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)

Tactic:
exact ⟨_, _, ⟨(triangleRotation _).counitIso.symm.app _ ≪≫ (rotate _).mapIso e ≪≫
  CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit φ⟩⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ (∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) → T ∈ distinguishedTriangles

Tactic:
rintro ⟨S, σ, ⟨e⟩⟩

Result:
case mpr.intro.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T ∈ distinguishedTriangles