awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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
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)
⊢ 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))
have 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)
Tactic: rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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
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)
⊢ 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))
have 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))
Tactic: rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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
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))
⊢ 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))
have 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))
Tactic: rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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
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))
⊢ 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))
have rw₅ : x₁ ≫ S.f.f j = x₂ ≫ CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i) (S.X₂.fromOpcycles 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₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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
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
⊢ 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))
have rw₇ : x₂ ≫ S.X₂.d i j = x₂ ≫ S.X₂.d 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₁]
-- 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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
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✝
have 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))
Tactic: dsimp
-- 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₁ S₂ : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
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✝
have 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))
Tactic: dsimp [Precomp.map]
-- 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₂ : 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)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos : ∀ (hi : ∃ (j : ι), c.Rel i j), Mono (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₂ : 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)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have neg : ∀ (hi : ¬∃ (j : ι), c.Rel i j), Mono (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₂ : 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)
have pos : ∀ (j : ι) (hij : c.Rel i j), Mono (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₂ : 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 := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos : (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₁ i j hij)).Exact
Tactic: apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δ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₂ : 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
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have pos₁ : (Functor.obj (δlastFunctor ⋙ δlastFunctor) (composableArrows₅ hS₂ i j hij)).Exact
Tactic: apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δ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₂ : 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
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δ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₂ : 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)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δ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₂ : 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)
⊢ Mono (X := S₁.X₃.homology i) (Y := S₂.X₃.homology i) (homologyMap φ.τ₃ i)
have 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)
Tactic: apply mono_of_epi_of_mono_of_mono
      ((δlastFunctor ⋙ δ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₂ : 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)
have 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)
Tactic: refine mono_of_epi_of_epi_of_mono (mapComposableArrows₂ φ i)
      (composableArrows₂_exact hS₁ i) (composableArrows₂_exact hS₂ i) ?_ h₁ h₂
-- 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₂ : 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 ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
have this : Epi S₁.g
Tactic: have := hS₁.epi_g
-- 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₂ : 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
⊢ Epi ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
have neg : ∀ (j : ι), ¬c.Rel i j
Tactic: apply epi_homologyMap_of_epi_of_not_rel