-- Mathlib/Algebra/Homology/HomologySequence.lean
/-- The diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j` is exact
when `c.Rel i j`. -/
lemma composableArrows₃_exact [CategoryWithHomology C] :
    (composableArrows₃ K i j).Exact

Proof state:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
⊢ (composableArrows₃ K i j).Exact

Tactic:
let T := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) (by simp)

Result:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
⊢ (composableArrows₃ K i j).Exact

Proof state:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (composableArrows₃ K i j).Exact

Tactic:
have hT : T.Exact := by
  rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
  exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))

Result:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).Exact

Proof state:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S.Exact

Tactic:
rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]

Result:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S'.Exact

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝ : CategoryWithHomology C
⊢ K.homologyι i ≫ K.opcyclesToCycles i j = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
⊢ K.homologyι i ≫ K.fromOpcycles i j = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T.Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]

Result:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T'.Exact

Proof state:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T'.Exact

Tactic:
exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))

Result:
no goals

Proof state:
case h₀
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex C := ShortComplex.mk (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C := ShortComplex.mk (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex C := ShortComplex.mk (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).δ₀.Exact

Tactic:
exact hT.exact_toComposableArrows

Result:
no goals