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 : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
      g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.SnakeInput.L₁', 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
A : C
x₃ : A ⟶ S.X₃.homology i
x₂ : A ⟶ S.X₂.opcycles i
x₁ : A ⟶ S.X₁.cycles j
h₂ : x₂ ≫ HomologicalComplex.opcyclesMap S.g i = x₃ ≫ S.X₃.homologyι i
h₁ : Eq (α := A ⟶ S.X₂.cycles j) (x₁ ≫ HomologicalComplex.cyclesMap S.f j) (x₂ ≫ S.X₂.opcyclesToCycles i j)
⊢ x₃ ≫ hS.δ i j hij = x₁ ≫ S.X₁.homologyπ j

Tactic:
(snakeInput hS i j hij).δ_eq x₃ x₂ x₁ h₂ h₁

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.cycles, HomologicalComplex.homology, CategoryTheory.ShortComplex.SnakeInput.δ_eq, CategoryTheory.ShortComplex.ShortExact.δ, 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 : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ 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 : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₃ : x₂ ≫ S.X₂.d i j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₄ : x₂ ≫ 0 = 0 ≫ S.f.f k
rw₅ : Eq (α := A ⟶ S.X₂.X k) 0 (0 ≫ S.f.f k)
rw₆ rw₇ : Eq.{v_1 + 1} (α := A ⟶ S.X₂.X k) 0 0
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.Hom.f, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_mono, HomologicalComplex.d_comp_d, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, HomologicalComplex.Hom.comm
-- 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
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ Eq (α := A ⟶ S.X₃.opcycles i)
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i) (HomologicalComplex.opcyclesMap S.g i))
    ((S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i) ≫ S.X₃.homologyι i)

Tactic:
simp only [assoc, HomologicalComplex.p_opcyclesMap,
        HomologicalComplex.homology_π_ι,
        HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.p_opcyclesMap, HomologicalComplex.liftCycles_i_assoc, HomologicalComplex.homology_π_ι
-- 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
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
rw :
  CategoryStruct.comp (Y := S.X₂.cycles j)
      (CategoryStruct.comp (Y := S.X₁.cycles j) (S.X₁.liftCycles x₁ k hk ⋯) (HomologicalComplex.cyclesMap S.f j))
      (S.X₂.iCycles j) =
    CategoryStruct.comp (Y := S.X₂.cycles j)
      (CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i) (S.X₂.opcyclesToCycles i j)) (S.X₂.iCycles j)
rw₁ :
  CategoryStruct.comp (Y := S.X₂.cycles j) (S.X₂.liftCycles (x₁ ≫ S.f.f j) k hk ⋯) (S.X₂.iCycles j) =
    CategoryStruct.comp (Y := S.X₂.cycles j)
      (CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i) (S.X₂.opcyclesToCycles i j)) (S.X₂.iCycles j)
rw₂ :
  x₁ ≫ S.f.f j =
    CategoryStruct.comp (Y := S.X₂.cycles j)
      (CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i) (S.X₂.opcyclesToCycles i j)) (S.X₂.iCycles j)
rw₃ :
  x₁ ≫ S.f.f j =
    CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i)
      (CategoryStruct.comp (Y := S.X₂.cycles j) (S.X₂.opcyclesToCycles i j) (S.X₂.iCycles j))
rw₄ :
  x₁ ≫ S.f.f j =
    x₂ ≫
      CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
        (CategoryStruct.comp (Y := S.X₂.cycles j) (S.X₂.opcyclesToCycles i j) (S.X₂.iCycles j))
rw₅ : x₁ ≫ S.f.f j = x₂ ≫ CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i) (S.X₂.fromOpcycles i j)
rw₆ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
rw₇ rw₈ : x₂ ≫ S.X₂.d i j = x₂ ≫ S.X₂.d i j
⊢ Eq (α := A ⟶ S.X₂.cycles j)
    (CategoryStruct.comp (Y := S.X₁.cycles j) (S.X₁.liftCycles x₁ k hk ⋯) (HomologicalComplex.cyclesMap S.f j))
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (x₂ ≫ S.X₂.pOpcycles i) (S.X₂.opcyclesToCycles i j))

Tactic:
rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.liftCycles_comp_cyclesMap, HomologicalComplex.p_fromOpcycles, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.liftCycles_i, HomologicalComplex.opcyclesToCycles_iCycles, CategoryTheory.ShortComplex.X₂
-- 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
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = S.X₁.liftCycles x₁ k hk ⋯ ≫ S.X₁.homologyπ j

Tactic:
simpa only [assoc] using hS.δ_eq' i j hij (S.X₃.liftCycles x₃ j
    (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i)
    (x₂ ≫ S.X₂.pOpcycles i) (S.X₁.liftCycles x₁ k hk _)
      (by simp only [assoc, HomologicalComplex.p_opcyclesMap,
        HomologicalComplex.homology_π_ι,
        HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂])
      (by rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁])

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.ShortExact.δ_eq', CategoryTheory.ShortComplex.X₁, CategoryTheory.CategoryStruct.comp, HomologicalComplex.pOpcycles, HomologicalComplex.liftCycles, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.X₂, ComplexShape.next_eq'
-- 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
hi : IsZero.{v_1, u_1} (S.X₂.homology i)
⊢ Mono (hS.δ i j hij)

Tactic:
(HomologicalComplex.HomologySequence.snakeInput _ _ _ _).mono_δ hi

Premises used: HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.mono_δ, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- 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
hj : IsZero.{v_1, u_1} (S.X₂.homology j)
⊢ Epi (hS.δ i j hij)

Tactic:
(HomologicalComplex.HomologySequence.snakeInput _ _ _ _).epi_δ hj

Premises used: HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.SnakeInput.epi_δ, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- 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
hi : IsZero.{v_1, u_1} (S.X₂.homology i)
hj : IsZero.{v_1, u_1} (S.X₂.homology j)
⊢ IsIso (hS.δ i j hij)

Tactic:
(HomologicalComplex.HomologySequence.snakeInput _ _ _ _).isIso_δ hi hj

Premises used: HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.isIso_δ, CategoryTheory.ShortComplex.homology, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i j : ι
hij : c.Rel i j
⊢ hS₁.δ i j hij ≫ homologyMap φ.τ₁ j = homologyMap φ.τ₃ i ≫ hS₂.δ i j hij

Tactic:
ShortComplex.SnakeInput.naturality_δ (mapSnakeInput φ hS₁ hS₂ i j hij)

Premises used: CategoryTheory.ShortComplex.SnakeInput.naturality_δ, CategoryTheory.ShortComplex.leftHomologyMap', HomologicalComplex.HomologySequence.mapSnakeInput, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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 : ι
⊢ (composableArrows₂ S₁ i).Exact

Tactic:
(hS₁.homology_exact₂ i).exact_toComposableArrows

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.toComposableArrows, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ComposableArrows.precomp, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, HomologicalComplex.homologyMap, HomologicalComplex.HomologySequence.composableArrows₂, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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
⊢ (composableArrows₅ hS₁ i j hij).Exact

Tactic:
exact_of_δ₀ (hS₁.homology_exact₂ i).exact_toComposableArrows
    (exact_of_δ₀ (hS₁.homology_exact₃ i j hij).exact_toComposableArrows
      (exact_of_δ₀ (hS₁.homology_exact₁ i j hij).exact_toComposableArrows
        (hS₁.homology_exact₂ j).exact_toComposableArrows))

Premises used: CategoryTheory.ShortComplex.ShortExact.homology_exact₃, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, CategoryTheory.ComposableArrows.exact_of_δ₀, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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 S₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
dsimp :
  Eq (α := S₁.X₁.homology i ⟶ S₂.X₂.homology i)
    (CategoryStruct.comp (Y := S₁.X₂.homology i) (homologyMap S₁.f i) (homologyMap φ.τ₂ i))
    (CategoryStruct.comp (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i) (homologyMap S₂.f i))
⊢ (composableArrows₂ S₁ i).map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ homologyMap φ.τ₂ i =
    homologyMap φ.τ₁ i ≫ (composableArrows₂ S₂ i).map' 0 1 homMk₁._proof_4 _proof_246✝

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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 S₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
⊢ Eq (α := S₁.X₁.homology i ⟶ S₂.X₂.homology i)
    (CategoryStruct.comp (Y := S₁.X₂.homology i) (homologyMap S₁.f i) (homologyMap φ.τ₂ i))
    (CategoryStruct.comp (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i) (homologyMap S₂.f i))

Tactic:
simp only [← homologyMap_comp, φ.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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 S₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
dsimp :
  Eq (α :=
    S₁.X₂.homology i ⟶
      Precomp.obj (mk₁ (X₀ := S₂.X₂.homology i) (X₁ := S₂.X₃.homology i) (homologyMap S₂.g i)) (S₂.X₁.homology i) 2)
    (CategoryStruct.comp (Y :=
      Precomp.obj (mk₁ (X₀ := S₁.X₂.homology i) (X₁ := S₁.X₃.homology i) (homologyMap S₁.g i)) (S₁.X₁.homology i) 2)
      (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
⊢ (composableArrows₂ S₁ i).map' 1 2 _proof_246✝ _proof_247✝ ≫ homologyMap φ.τ₃ i =
    homologyMap φ.τ₂ i ≫ (composableArrows₂ S₂ i).map' 1 2 _proof_246✝ _proof_247✝

Tactic:
dsimp [Precomp.map]

Premises used: CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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 S₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
⊢ Eq (α :=
    S₁.X₂.homology i ⟶
      Precomp.obj (mk₁ (X₀ := S₂.X₂.homology i) (X₁ := S₂.X₃.homology i) (homologyMap S₂.g i)) (S₂.X₁.homology i) 2)
    (CategoryStruct.comp (Y :=
      Precomp.obj (mk₁ (X₀ := S₁.X₂.homology i) (X₁ := S₁.X₃.homology i) (homologyMap S₁.g i)) (S₁.X₁.homology i) 2)
      (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))

Tactic:
simp only [← homologyMap_comp, φ.comm₂₃]

Premises used: HomologicalComplex.homologyMap_comp, CategoryTheory.ShortComplex.Hom.comm₂₃
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
pos : ∀ (hi : ∃ (j : ι), c.Rel i j), Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
neg : ∀ (hi : ¬∃ (j : ι), c.Rel i j), Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
by_cases hi : ∃ j, c.Rel i j
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
hi : ∃ (j : ι), c.Rel i j
pos : ∀ (j : ι) (hij : c.Rel i j), Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
obtain ⟨j, hij⟩ := hi
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
pos : (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact
pos₁ : (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact
pos₂ :
  Epi (X :=
    (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 0
      mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (CategoryTheory.Functor.map (δlastFunctor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)
pos₃ :
  Mono (X :=
    (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 1
      mono_of_epi_of_mono_of_mono'._proof_11)
    (app' (CategoryTheory.Functor.map (δlastFunctor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)
pos₄ :
  Mono (X :=
    (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 3
      mono_of_epi_of_mono_of_mono'._proof_7)
    (app' (CategoryTheory.Functor.map (δlastFunctor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))

Premises used: CategoryTheory.ComposableArrows.δlastFunctor, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, HomologicalComplex.HomologySequence.mapComposableArrows₅
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact

Tactic:
(composableArrows₅_exact hS₁ i j hij).δlast.δlast

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.whiskerLeft, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₁ i j hij).δlast.δlast

Premises used: HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact

Tactic:
(composableArrows₅_exact hS₂ i j hij).δlast.δlast

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.whiskerLeft, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₂ : Mono (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₂ i j hij).δlast.δlast

Premises used: HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast