-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma exists_iso_binaryBiproduct_of_distTriang (T : Triangle C) (hT : T ∈ distTriang C)
    (zero : T.mor₃ = 0) :
    ∃ (e : T.obj₂ ≅ T.obj₁ ⊞ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧
      T.mor₂ = e.hom ≫ biprod.snd

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom = biprod.inl

Tactic:
ext

Result:
case intro.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.fst = biprod.inl ≫ biprod.fst

case intro.h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.snd = biprod.inl ≫ biprod.snd

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
refine ⟨biprod.uniqueUpToIso _ _ d.isBilimit, ⟨?_, by simp [d]⟩⟩

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom = biprod.inl

Proof state:
case intro.h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.fst = biprod.inl ≫ biprod.fst

Tactic:
simpa [d] using d.bicone.inl_fst

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
have := T.epi₂ hT zero

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this : Epi T.mor₂
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ T.mor₂ = (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom ≫ biprod.snd

Tactic:
simp [d]

Result:
no goals

Proof state:
case intro.h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.snd = biprod.inl ≫ biprod.snd

Tactic:
simpa [d] using d.bicone.inl_snd

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
⊢ (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) ≫ T.mor₂ = 0

Tactic:
simp

Result:
no goals

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
let d := binaryBiproductData _ hT zero (section_ T.mor₂) (by simp) fst
  (by simp only [← hfst, sub_add_cancel])

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ fst ≫ T.mor₁ + T.mor₂ ≫ section_ T.mor₂ = 𝟙 T.obj₂

Tactic:
simp only [← hfst, sub_add_cancel]

Result:
no goals