-- Mathlib/Algebra/Homology/HomologySequence.lean
/-- Exactness of `S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i`. -/
lemma homology_exact₂ : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i)
    (HomologicalComplex.homologyMap S.g i) (by rw [← HomologicalComplex.homologyMap_comp,
      S.zero, HomologicalComplex.homologyMap_zero])).Exact

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this : Epi S.g
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) :=
  fun K => ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)

Result:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
have := hS.epi_g

Result:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this : Epi S.g
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
by_cases h : c.Rel i (c.next i)

Result:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : c.Rel i (c.next i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{?u.127946, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i = 0

Tactic:
rw [← HomologicalComplex.homologyMap_comp,
S.zero, HomologicalComplex.homologyMap_zero]

Result:
no goals

Proof state:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : c.Rel i (c.next i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
exact (snakeInput hS i _ h).L₀_exact

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₂.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).g =
    (S.map (HomologicalComplex.homologyFunctor C c i)).g ≫ (asIso (S.X₃.homologyι i)).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₁.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).f =
    (S.map (HomologicalComplex.homologyFunctor C c i)).f ≫ (asIso (S.X₂.homologyι i)).hom

Tactic:
simp

Result:
no goals

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
have e : S.map (HomologicalComplex.homologyFunctor C c i) ≅
    S.map (HomologicalComplex.opcyclesFunctor C c i) :=
  ShortComplex.isoMk (asIso (S.X₁.homologyι i))
    (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by simp) (by simp)

Result:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
e : S.map (HomologicalComplex.homologyFunctor C c i) ≅ S.map (HomologicalComplex.opcyclesFunctor C c i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
e : S.map (HomologicalComplex.homologyFunctor C c i) ≅ S.map (HomologicalComplex.opcyclesFunctor C c i)
⊢ (ShortComplex.mk (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i) ⋯).Exact

Tactic:
exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)

Result:
no goals