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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
have refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
have refine_1₂ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) 0
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₂ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) 0
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
have refine_1₃ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.X₂.pOpcycles i ≫ k) 0
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₂ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₃ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.X₂.pOpcycles i ≫ k) 0
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
have refine_1₄ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (0 ≫ k) 0
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₂ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₃ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.X₂.pOpcycles i ≫ k) 0
refine_1₄ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (0 ≫ k) 0
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
have refine_1₅ : Eq.{v_1 + 1} (α := S.X₂.X (c.prev i) ⟶ A) 0 0
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k
have refine_2 : CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
    (CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) sorry sorry)) =
  S.X₂.pOpcycles i ≫ k
Tactic: rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
        (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯)) =
    S.X₂.pOpcycles i ≫ k
⊢ CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k
have refine_2₁ : CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
    (S.X₂.descOpcycles (S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) (c.prev i) sorry sorry) =
  S.X₂.pOpcycles i ≫ k
Tactic: rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
        (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯)) =
    S.X₂.pOpcycles i ≫ k
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (S.X₂.descOpcycles (S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) (c.prev i) ⋯ ⋯) =
    S.X₂.pOpcycles i ≫ k
⊢ CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k
have refine_2₂ : S.g.f i ≫ (↑H : S.X₃.X i ⟶ A) = S.X₂.pOpcycles i ≫ k
Tactic: rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]
-- 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.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
        (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯)) =
    S.X₂.pOpcycles i ≫ k
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (S.X₂.descOpcycles (S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) (c.prev i) ⋯ ⋯) =
    S.X₂.pOpcycles i ≫ k
refine_2₂ : S.g.f i ≫ (↑H : S.X₃.X i ⟶ A) = S.X₂.pOpcycles i ≫ k
⊢ CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k
have refine_2₃ : S.X₂.pOpcycles i ≫ k = S.X₂.pOpcycles i ≫ k
Tactic: rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (CategoryStruct.comp (Y := S.X₂.cycles i) (cyclesMap S.f i) (cyclesMap S.g i))
    0
have rw : Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap (S.f ≫ S.g) i) 0
Tactic: rw [← cyclesMap_comp, S.zero, cyclesMap_zero]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
rw : Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap (S.f ≫ S.g) i) 0
⊢ Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (CategoryStruct.comp (Y := S.X₂.cycles i) (cyclesMap S.f i) (cyclesMap S.g i))
    0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap 0 i) 0
Tactic: rw [← cyclesMap_comp, S.zero, cyclesMap_zero]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
rw : Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap 0 i) 0
⊢ Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (CategoryStruct.comp (Y := S.X₂.cycles i) (cyclesMap S.f i) (cyclesMap S.g i))
    0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁.cycles i ⟶ S.X₃.cycles i) 0 0
Tactic: rw [← cyclesMap_comp, S.zero, cyclesMap_zero]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
have dsimp : Mono (S.f.f i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      ⋯).Exact
have this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
Tactic: have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
⊢ (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      ⋯).Exact
have have : ∀
  (hi :
    IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
      (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) sorry)),
  (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      sorry).Exact
Tactic: have hi := (hS.map (HomologicalComplex.eval C c i)).fIsKernel
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
⊢ (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      ⋯).Exact
have hS₁ : IsLimit
  (KernelFork.ofι
    (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
        (cyclesMap S.g i) sorry).f
    sorry)
Tactic: apply ShortComplex.exact_of_f_is_kernel
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k :
  A ⟶
    (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
        (cyclesMap S.g i) ⋯).X₂
hk :
  k ≫
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).g =
    0
⊢ { l :
    A ⟶
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).X₁ //
    l ≫
        (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
            (cyclesMap S.g i) ⋯).f =
      k }
have dsimp : { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
Tactic: dsimp at k hk ⊢
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
⊢ Eq (α := A ⟶ ShortComplex.X₃ (S.map (eval C c i))) ((k ≫ S.X₂.iCycles i) ≫ ShortComplex.g (S.map (eval C c i))) 0
have dsimp : (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
Tactic: dsimp
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
have rw : k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
Tactic: rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
rw : k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
have rw₁ : k ≫ CategoryStruct.comp (Y := S.X₃.cycles i) (cyclesMap S.g i) (S.X₃.iCycles i) = 0
Tactic: rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
rw : k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
rw₁ : k ≫ CategoryStruct.comp (Y := S.X₃.cycles i) (cyclesMap S.g i) (S.X₃.iCycles i) = 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
have rw₂ : Eq (α := A ⟶ S.X₃.X i) (CategoryStruct.comp (Y := S.X₃.cycles i) 0 (S.X₃.iCycles i)) 0
Tactic: rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp]
-- 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.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
rw : k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
rw₁ : k ≫ CategoryStruct.comp (Y := S.X₃.cycles i) (cyclesMap S.g i) (S.X₃.iCycles i) = 0
rw₂ : Eq (α := A ⟶ S.X₃.X i) (CategoryStruct.comp (Y := S.X₃.cycles i) 0 (S.X₃.iCycles i)) 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₃.X i) 0 0
Tactic: rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp]