awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)

Tactic:
h₁

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, 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₁ 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
⊢ 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)

Tactic:
exact h₁
-- 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
⊢ 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)

Tactic:
h₂

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, 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₁ 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
⊢ 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)

Tactic:
exact h₂
-- 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
⊢ 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)

Tactic:
h₃ _ hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, 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₁ 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
⊢ 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)

Tactic:
exact h₃ _ hij
-- 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
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
mono_of_epi_of_epi_of_mono (mapComposableArrows₂ φ i)
      (composableArrows₂_exact hS₁ i) (composableArrows₂_exact hS₂ i) ?_ h₁ h₂

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, HomologicalComplex.HomologySequence.mapComposableArrows₂, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.HomologySequence.composableArrows₂_exact, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono, 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₁ 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
neg : Epi ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
refine mono_of_epi_of_epi_of_mono (mapComposableArrows₂ φ i)
      (composableArrows₂_exact hS₁ i) (composableArrows₂_exact hS₂ i) ?_ h₁ h₂

Premises used: HomologicalComplex.HomologySequence.mapComposableArrows₂, HomologicalComplex.HomologySequence.composableArrows₂_exact, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono
-- 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
⊢ Epi S₁.g

Tactic:
have := hS₁.epi_g
-- 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
this : Epi S₁.g
neg : ∀ (j : ι), ¬c.Rel i j
⊢ Epi ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)

Tactic:
apply epi_homologyMap_of_epi_of_not_rel

Premises used: HomologicalComplex.epi_homologyMap_of_epi_of_not_rel
-- 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
this : Epi S₁.g
⊢ ∀ (j : ι), ¬c.Rel i j

Tactic:
simpa using 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
neg : ∀ (hi : ¬∃ (j : ι), c.Rel i j), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ Epi (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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ Epi (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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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 (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact
pos₁ : (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact
pos₂ :
  Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 0
      mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)
pos₃ :
  Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 2
      mono_of_epi_of_mono_of_mono'._proof_4)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)
pos₄ :
  Mono (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 3
      mono_of_epi_of_mono_of_mono'._proof_7)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

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

Premises used: CategoryTheory.ComposableArrows.δlastFunctor, CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, HomologicalComplex.HomologySequence.mapComposableArrows₅, CategoryTheory.ComposableArrows.δ₀Functor
-- 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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 (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact

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

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.whiskerLeft, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast, CategoryTheory.ComposableArrows.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₂ : 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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 (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact

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

Premises used: HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast, CategoryTheory.ComposableArrows.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₂ : 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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 (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact

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

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.whiskerLeft, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast, CategoryTheory.ComposableArrows.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₂ : 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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 (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact

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

Premises used: HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ComposableArrows.Exact.δlast, CategoryTheory.ComposableArrows.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₂ : 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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
⊢ Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 0
      mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

Tactic:
h₁

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, 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₁ 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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
⊢ Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 0
      mono_of_epi_of_mono_of_mono'._proof_13)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

Tactic:
exact h₁
-- 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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
⊢ Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 2
      mono_of_epi_of_mono_of_mono'._proof_4)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
h₂ j hij

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, 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₁ 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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
⊢ Epi (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 2
      mono_of_epi_of_mono_of_mono'._proof_4)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
exact h₂ j hij
-- 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₂ : ∀ (j : ι), c.Rel i j → Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
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
⊢ Mono (X :=
    (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).obj' 3
      mono_of_epi_of_mono_of_mono'._proof_7)
    (app' (CategoryTheory.Functor.map (δ₀Functor ⋙ δlastFunctor) (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
h₃ j hij

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap