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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯)
have h₁ : IsColimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₁)
  (Functor.mapCocone ShortComplex.π₁ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
⊢ IsColimit (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯)
have h₂ : IsColimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₂)
  (Functor.mapCocone ShortComplex.π₂ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
h₂ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCocone ShortComplex.π₂ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
⊢ IsColimit (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯)
have h₃ : IsColimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₃)
  (Functor.mapCocone ShortComplex.π₃ (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S)
have this : Epi S.g
Tactic: have := hS.epi_g
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Epi (X := ShortComplex.X₂ (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))
    (ShortComplex.g (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))
have this : Epi S.g
Tactic: have := hS.epi_g
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Epi S.g
⊢ Epi (X := ShortComplex.X₂ (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))
    (ShortComplex.g (Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S))
have dsimp : Epi (X := S.X₂.opcycles i) (Y := S.X₃.opcycles i) (opcyclesMap S.g 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ ShortComplex.Exact (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
have this : Mono S.f
Tactic: have := hS.mono_f
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ Mono (X := ShortComplex.X₁ (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))
    (ShortComplex.f (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))
have this : Mono S.f
Tactic: have := hS.mono_f
-- 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_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
this : Mono S.f
⊢ Mono (X := ShortComplex.X₁ (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))
    (ShortComplex.f (Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S))
have dsimp : Mono (X := S.X₁.cycles j) (Y := S.X₂.cycles j) (cyclesMap S.f j)
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.ShortExact
i j : ι
hij : c.Rel i j
⊢ Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i))
    0
have rw : Eq (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap (S.f ≫ S.g) i) 0
Tactic: rw [← HomologicalComplex.homologyMap_comp,
      S.zero, HomologicalComplex.homologyMap_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.ShortExact
i j : ι
hij : c.Rel i j
rw : Eq (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap (S.f ≫ S.g) i) 0
⊢ Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i))
    0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap 0 i) 0
Tactic: rw [← HomologicalComplex.homologyMap_comp,
      S.zero, HomologicalComplex.homologyMap_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.ShortExact
i j : ι
hij : c.Rel i j
rw : Eq (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.homology i ⟶ S.X₃.homology i) (HomologicalComplex.homologyMap 0 i) 0
⊢ Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i))
    0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁.homology i ⟶ S.X₃.homology i) 0 0
Tactic: rw [← HomologicalComplex.homologyMap_comp,
      S.zero, HomologicalComplex.homologyMap_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.ShortExact
i : ι
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have pos : ∀ (h : c.Rel i (c.next i)),
  { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: by_cases h : c.Rel i (c.next i)
-- 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 : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
        g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have neg : ∀ (h : ¬c.Rel i (c.next i)),
  { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: by_cases h : c.Rel i (c.next i)
-- 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.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have this : Epi S.g
Tactic: have := hS.epi_g
-- 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.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this : Epi S.g
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have this₁ : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
Tactic: have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) :=
      fun K => ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)
-- 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 : ι
h : ¬c.Rel i (c.next i)
this_1 : Epi S.g
this : ∀ (K : HomologicalComplex.{v_1, u_1, u_2} C c), IsIso (X := K.homology i) (K.homologyι i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have neg : ∀
  (e :
    Iso (C := ShortComplex.{v_1, u_1} C) (S.map (HomologicalComplex.homologyFunctor C c i))
      (S.map (HomologicalComplex.opcyclesFunctor C c i))),
  { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: have e : S.map (HomologicalComplex.homologyFunctor C c i) ≅
        S.map (HomologicalComplex.opcyclesFunctor C c i) :=
      ShortComplex.isoMk (asIso (S.X₁.homologyι i))
        (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by simp) (by simp)
-- 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.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
⊢ x₁ ≫ S.X₁.d j k = 0
have this : Mono S.f
Tactic: have := hS.mono_f
-- 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
this : Mono S.f
⊢ x₁ ≫ S.X₁.d j k = 0
have rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₃ : x₂ ≫ S.X₂.d i j ≫ S.X₂.d j k = 0 ≫ S.f.f k
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₃ : x₂ ≫ S.X₂.d i j ≫ S.X₂.d j k = 0 ≫ S.f.f k
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₄ : x₂ ≫ 0 = 0 ≫ S.f.f k
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₃ : x₂ ≫ S.X₂.d i j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₄ : x₂ ≫ 0 = 0 ≫ S.f.f k
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₅ : Eq (α := A ⟶ S.X₂.X k) 0 (0 ≫ S.f.f k)
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
this : Mono S.f
rw : (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k
rw₁ : x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
rw₂ : x₁ ≫ S.f.f j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₃ : x₂ ≫ S.X₂.d i j ≫ S.X₂.d j k = 0 ≫ S.f.f k
rw₄ : x₂ ≫ 0 = 0 ≫ S.f.f k
rw₅ : Eq (α := A ⟶ S.X₂.X k) 0 (0 ≫ S.f.f k)
⊢ x₁ ≫ S.X₁.d j k = 0
have rw₆ : Eq.{v_1 + 1} (α := A ⟶ S.X₂.X k) 0 0
Tactic: rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, 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.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
⊢ 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 : CategoryStruct.comp (Y := S.X₂.cycles j)
    (CategoryStruct.comp (Y := S.X₁.cycles j) (S.X₁.liftCycles x₁ k hk sorry) (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)
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)
⊢ 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₁ : CategoryStruct.comp (Y := S.X₂.cycles j) (S.X₂.liftCycles (x₁ ≫ S.f.f j) k hk sorry) (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)
Tactic: rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
        HomologicalComplex.p_fromOpcycles, hx₁]