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₂ : ∀ (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:
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)
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₂ : ∀ (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
this : Epi S₂.g
⊢ Eq (α := Functor.obj (homologyFunctor C c i) S₁.X₂ ⟶ Functor.obj (homologyFunctor C c i) S₂.X₃)
    (CategoryTheory.Functor.map (homologyFunctor C c i) (φ.τ₂ ≫ S₂.g))
    (CategoryTheory.Functor.map (homologyFunctor C c i) (S₁.g ≫ φ.τ₃))

Tactic:
have eq := (homologyFunctor C _ i).congr_map φ.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₂ : ∀ (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
this : Epi S₂.g
eq : Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i) (homologyMap (φ.τ₂ ≫ S₂.g) i) (homologyMap (S₁.g ≫ φ.τ₃) i)
⊢ Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i)
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
    (CategoryStruct.comp (Y := S₁.X₃.homology i) (homologyMap S₁.g i) (homologyMap φ.τ₃ i))

Tactic:
simp only [homologyMap_comp] at eq

Premises used: 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₂ : 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
this : Epi S₂.g
eq :
  Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i)
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
    (CategoryStruct.comp (Y := S₁.X₃.homology i) (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
⊢ ∀ (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)
hi : ¬∃ (j : ι), c.Rel i j
this : Epi S₂.g
eq :
  Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i)
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
    (CategoryStruct.comp (Y := S₁.X₃.homology i) (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
⊢ Epi (X := S₂.X₂.homology i) (Y := S₂.X₃.homology i) (homologyMap S₂.g i)

Tactic:
have := epi_homologyMap_of_epi_of_not_rel S₂.g i (by 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)
hi : ¬∃ (j : ι), c.Rel i j
this_1 : Epi S₂.g
eq :
  Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i)
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
    (CategoryStruct.comp (Y := S₁.X₃.homology i) (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
this : Epi (X := S₂.X₂.homology i) (Y := S₂.X₃.homology i) (homologyMap S₂.g i)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
epi_of_epi_fac eq.symm

Premises used: CategoryTheory.epi_of_epi_fac, Eq.symm
-- 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
this_1 : Epi S₂.g
eq :
  Eq (α := S₁.X₂.homology i ⟶ S₂.X₃.homology i)
    (CategoryStruct.comp (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i) (homologyMap S₂.g i))
    (CategoryStruct.comp (Y := S₁.X₃.homology i) (homologyMap S₁.g i) (homologyMap φ.τ₃ i))
this : Epi (X := S₂.X₂.homology i) (Y := S₂.X₃.homology i) (homologyMap S₂.g i)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
exact epi_of_epi_fac eq.symm

Premises used: CategoryTheory.epi_of_epi_fac, Eq.symm
-- 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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
⊢ IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)

Tactic:
have := 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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
this : IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
⊢ Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)

Tactic:
infer_instance
-- 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
have := mono_homologyMap_τ₃ φ hS₁ hS₂ i h₁ (IsIso.mono_of_iso _) (fun j hij => by
    have := h₃ j hij
    infer_instance)
-- 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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)
this : Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
⊢ IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)

Tactic:
have := 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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)
this_1 : Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
this : IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
⊢ Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)

Tactic:
infer_instance
-- 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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)
this : Mono (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:
have := epi_homologyMap_τ₃ φ hS₁ hS₂ i inferInstance (fun j hij => by
    have := h₃ j hij
    infer_instance) 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₂ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (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)
this_1 : Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
this : Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
rw : ∀ (i : ι), QuasiIsoAt φ.τ₃ i
⊢ QuasiIso φ.τ₃

Tactic:
rw [quasiIso_iff]

Premises used: quasiIso_iff
-- 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
rw : IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
⊢ QuasiIsoAt φ.τ₃ i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
h₃ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
h₄ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
h₅ : ∀ (j : ι), c.Rel i j → IsIso (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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)

Tactic:
apply isIso_homologyMap_τ₃ φ hS₁ hS₂

Premises used: HomologicalComplex.HomologySequence.isIso_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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)

Tactic:
infer_instance
-- 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)

Tactic:
infer_instance
-- 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)

Tactic:
infer_instance
-- 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
h₁ : QuasiIso φ.τ₁
h₂ : QuasiIso φ.τ₂
i : ι
⊢ ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₂.homology j) (Y := S₂.X₂.homology j) (homologyMap φ.τ₂ j)

Tactic:
infer_instance
-- 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
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
rw : IsZero.{v_1, u_1} (S.X₁.homology j)
⊢ S.X₁.ExactAt j

Tactic:
rw [exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- 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
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
pos : ∀ (hj : ∃ (i : ι), c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
neg : ∀ (hj : ∀ (i : ι), ¬c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)

Tactic:
by_cases! hj : ∃ i, 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 : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∃ (i : ι), c.Rel i j
pos : ∀ (i : ι) (hij : c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)

Tactic:
obtain ⟨i, hij⟩ := hj
-- 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
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
⊢ Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)

Tactic:
have := h₂ i 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 : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
pos :
  { 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 }.f =
    0
pos₁ :
  { 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 }.g =
    0
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)

Tactic:
apply (hS.homology_exact₁ i j hij).isZero_X₂

Premises used: CategoryTheory.ShortComplex.ShortExact.homology_exact₁, CategoryTheory.ShortComplex.Exact.isZero_X₂
-- 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
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
⊢ { 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 }.f =
    0

Tactic:
simp [← cancel_epi (HomologicalComplex.homologyMap S.g i)]

Premises used: HomologicalComplex.homologyMap, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.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 : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
⊢ { 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 }.g =
    0

Tactic:
simp [← cancel_mono (HomologicalComplex.homologyMap S.g j),
        ← HomologicalComplex.homologyMap_comp]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.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 : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- 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
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this : Mono S.f
⊢ Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)

Tactic:
have := HomologicalComplex.mono_homologyMap_of_mono_of_not_rel S.f j hj