awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos : ∀ (hi : ∃ (j : ι), c.Rel i j), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
Tactic: by_cases hi : ∃ j, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have neg : ∀ (hi : ¬∃ (j : ι), c.Rel i j), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
Tactic: by_cases hi : ∃ j, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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 (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos : ∀ (j : ι) (hij : c.Rel i j), Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
Tactic: obtain ⟨j, hij⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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 := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos : (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact
Tactic: apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos₁ : (Functor.obj (δ₀Functor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact
Tactic: apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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 (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have this : Epi S₂.g
Tactic: have := hS₂.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have eq : 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₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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)
⊢ Epi (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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))
Tactic: simp only [homologyMap_comp] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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 φ.τ₃ i)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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
⊢ Mono (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
have this : IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
Tactic: have := h₃ j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have this : 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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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
⊢ Epi (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
have this₁ : IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
Tactic: have := h₃ j hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have this₁ : 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₄
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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 φ.τ₂
⊢ QuasiIso φ.τ₃
have rw : ∀ (i : ι), QuasiIsoAt φ.τ₃ i
Tactic: rw [quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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 : ι
⊢ QuasiIsoAt φ.τ₃ i
have rw : IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
have h₃ : Epi (X := S₁.X₁.homology i) (Y := S₂.X₁.homology i) (homologyMap φ.τ₁ i)
Tactic: apply isIso_homologyMap_τ₃ φ hS₁ hS₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have h₄ : IsIso (X := S₁.X₂.homology i) (Y := S₂.X₂.homology i) (homologyMap φ.τ₂ i)
Tactic: apply isIso_homologyMap_τ₃ φ hS₁ hS₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have h₅ : ∀ (j : ι), c.Rel i j → IsIso (X := S₁.X₁.homology j) (Y := S₂.X₁.homology j) (homologyMap φ.τ₁ j)
Tactic: apply isIso_homologyMap_τ₃ φ hS₁ hS₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ IsIso (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have h₆ : ∀ (j : ι), c.Rel i j → Mono (X := S₁.X₂.homology j) (Y := S₂.X₂.homology j) (homologyMap φ.τ₂ j)
Tactic: apply isIso_homologyMap_τ₃ φ hS₁ hS₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ S.X₁.ExactAt j
have rw : IsZero.{v_1, u_1} (S.X₁.homology j)
Tactic: rw [exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have pos : ∀ (hj : ∃ (i : ι), c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
Tactic: by_cases! hj : ∃ i, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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)
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have neg : ∀ (hj : ∀ (i : ι), ¬c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
Tactic: by_cases! hj : ∃ i, c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (goal)
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
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have pos : ∀ (i : ι) (hij : c.Rel i j), IsZero.{v_1, u_1} (S.X₁.homology j)
Tactic: obtain ⟨i, hij⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequenceLemmas (hypothesis)
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
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)
have this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
Tactic: have := h₂ i hij