awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCone ShortComplex.π₂ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))

Tactic:
exact (KernelFork.isLimitMapConeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 0).fIsKernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₃)
    (Functor.mapCone ShortComplex.π₃ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))

Tactic:
exact (KernelFork.isLimitMapConeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 0).fIsKernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
h₂ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCocone ShortComplex.π₂ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
h₃ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₃)
    (Functor.mapCocone ShortComplex.π₃ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
⊢ IsColimit (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯)

Tactic:
apply ShortComplex.isColimitOfIsColimitπ

Premises used: CategoryTheory.ShortComplex.isColimitOfIsColimitπ
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCocone ShortComplex.π₂ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₃)
    (Functor.mapCocone ShortComplex.π₃ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S)

Tactic:
opcycles_right_exact S hS.exact i

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.ShortExact.exact, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, HomologicalComplex.opcycles_right_exact, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap', CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.RightHomologyData.descQ
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S)

Tactic:
exact opcycles_right_exact S hS.exact i

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, HomologicalComplex.opcycles_right_exact
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
dsimp : Epi (X := S.X₂.opcycles i) (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
⊢ Epi (X := ShortComplex.X₂ (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))
    (ShortComplex.g (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
⊢ Epi (X := S.X₂.opcycles i) (Y := S.X₃.opcycles i) (opcyclesMap S.g i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)

Tactic:
cycles_left_exact S hS.exact j

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.ShortExact.exact, CategoryTheory.ShortComplex.cyclesMap', HomologicalComplex.cycles_left_exact, CategoryTheory.ShortComplex.cyclesMap, HomologicalComplex.cyclesMap, CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.cycles, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)

Tactic:
exact cycles_left_exact S hS.exact j

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, HomologicalComplex.cycles_left_exact
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
dsimp : Mono (X := S.X₁.cycles j) (Y := S.X₂.cycles j) (cyclesMap S.f j)
⊢ Mono (X := ShortComplex.X₁ (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))
    (ShortComplex.f (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
⊢ Mono (X := S.X₁.cycles j) (Y := S.X₂.cycles j) (cyclesMap S.f j)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Eq (α := S.X₃.homology i ⟶ S.X₂.homology j) (hS.δ i j hij ≫ HomologicalComplex.homologyMap S.f j) 0

Tactic:
(snakeInput hS i j hij).δ_L₃_f

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f, HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Eq (α := S.X₂.homology i ⟶ S.X₁.homology j) (HomologicalComplex.homologyMap S.g i ≫ hS.δ i j hij) 0

Tactic:
(snakeInput hS i j hij).L₀_g_δ

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
      g := HomologicalComplex.homologyMap S.f j, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

Tactic:
(snakeInput hS i j hij).L₂'_exact

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.SnakeInput.L₂', HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
rw : Eq (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap 0 i) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁.homology i ⟶ S.X₃.homology i) 0 0
⊢ Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i))
    0

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

Premises used: HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_zero, CategoryTheory.ShortComplex.zero
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
        g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
neg :
  ∀ (h : ¬c.Rel i (c.next i)),
    { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
        g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : c.Rel i (c.next i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.map, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : c.Rel i (c.next i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.L₀_exact
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this : Epi S.g
⊢ ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)

Tactic:
have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) :=
      fun K => ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
⊢ Eq (α :=
    X₁ (S.map (HomologicalComplex.homologyFunctor C c i)) ⟶ X₂ (S.map (HomologicalComplex.opcyclesFunctor C c i)))
    (Iso.hom (asIso (S.X₁.homologyι i)) ≫ f (S.map (HomologicalComplex.opcyclesFunctor C c i)))
    (f (S.map (HomologicalComplex.homologyFunctor C c i)) ≫ Iso.hom (asIso (S.X₂.homologyι i)))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
⊢ Eq (α :=
    X₂ (S.map (HomologicalComplex.homologyFunctor C c i)) ⟶ X₃ (S.map (HomologicalComplex.opcyclesFunctor C c i)))
    (Iso.hom (asIso (S.X₂.homologyι i)) ≫ g (S.map (HomologicalComplex.opcyclesFunctor C c i)))
    (g (S.map (HomologicalComplex.homologyFunctor C c i)) ≫ Iso.hom (asIso (S.X₃.homologyι i)))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
neg :
  ∀
    (e :
      Iso (C := ShortComplex.{v_1, u_1} C) (S.map (HomologicalComplex.homologyFunctor C c i))
        (S.map (HomologicalComplex.opcyclesFunctor C c i))),
    { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
        g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.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)
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
e :
  Iso (C := ShortComplex.{v_1, u_1} C) (S.map (HomologicalComplex.homologyFunctor C c i))
    (S.map (HomologicalComplex.opcyclesFunctor C c i))
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, HomologicalComplex.opcycles_right_exact, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
e :
  Iso (C := ShortComplex.{v_1, u_1} C) (S.map (HomologicalComplex.homologyFunctor C c i))
    (S.map (HomologicalComplex.opcyclesFunctor C c i))
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, HomologicalComplex.opcycles_right_exact, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Iso.symm