-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
/-- Is `S` is an exact short complex and `h : S.HomologyData`, there is
a short exact sequence `0 ⟶ h.left.K ⟶ S.X₂ ⟶ h.right.Q ⟶ 0`. -/
lemma Exact.shortExact {S : ShortComplex C} (hS : S.Exact) (h : S.HomologyData) :
    (ShortComplex.mk _ _ (h.exact_iff_i_p_zero.1 hS)).ShortExact where
  exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this : Epi h.left.f'
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
have := hS.mono_g' h.right

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
let a : S ⟶ S' :=
  { τ₁ := h.left.f'
    τ₂ := 𝟙 _
    τ₃ := 𝟙 _ }

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
let S' := ShortComplex.mk h.left.i S.g (by simp)

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
⊢ h.left.i ≫ S.g = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
have := hS.epi_f' h.left

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this : Epi h.left.f'
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
rwa [ShortComplex.exact_iff_of_epi_of_isIso_of_mono b,
  ← ShortComplex.exact_iff_of_epi_of_isIso_of_mono a]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
let b : S'' ⟶ S' :=
  { τ₁ := 𝟙 _
    τ₂ := 𝟙 _
    τ₃ := h.right.g' }

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact

Tactic:
let S'' := ShortComplex.mk _ _ (h.exact_iff_i_p_zero.1 hS)

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := ShortComplex.mk h.left.i S.g ⋯
S'' : ShortComplex C := ShortComplex.mk h.left.i h.right.p ⋯
⊢ (ShortComplex.mk h.left.i h.right.p ⋯).Exact