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 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hij : c.Rel i j
inst_2 : K.HasHomology i
inst_3 : K.HasHomology j
⊢ Epi
    ((composableArrows₃ K i j).map' 2 3 instEpiMap'ComposableArrows₃OfNatNat._proof_2
      instEpiMap'ComposableArrows₃OfNatNat._proof_3)
have dsimp : Epi (X := K.cycles j) (K.homologyπ j)
Tactic: dsimp [-Fin.reduceFinMk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S.Exact
have rw : S'.Exact
Tactic: rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (hypothesis)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (composableArrows₃ K i j).Exact
have hS : S.Exact
Tactic: have hS : S.Exact := by
    rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]
    exact S'.exact_of_f_is_kernel (K.homologyIsKernel i j (c.next_eq' hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T.Exact
have rw : T'.Exact
Tactic: rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (hypothesis)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (composableArrows₃ K i j).Exact
have hT : T.Exact
Tactic: have hT : T.Exact := by
    rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
    exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).Exact
have h : (ComposableArrows.mk₂ (X₀ := (composableArrows₃ K i j).obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₁ :=
    (composableArrows₃ K i j).obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₂ :=
    (composableArrows₃ K i j).obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 sorry :
      (composableArrows₃ K i j).obj (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
        (composableArrows₃ K i j).obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
    ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 sorry :
      (composableArrows₃ K i j).obj (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
        (composableArrows₃ K i j).obj (⟨2, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact
Tactic: apply ComposableArrows.exact_of_δ₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
h :
  (ComposableArrows.mk₂ (X₀ := (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₁ :=
      (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₂ :=
      (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 ⋯ :
        (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 ⋯ :
        (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact
⊢ (composableArrows₃ K i j).Exact
have h₀ : (composableArrows₃ K i j).δ₀.Exact
Tactic: apply ComposableArrows.exact_of_δ₀
-- 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
⊢ Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i)
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (opcyclesMap S.f i) (opcyclesMap S.g i)) 0
have rw : Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap (S.f ≫ S.g) i) 0
Tactic: rw [← opcyclesMap_comp, S.zero, opcyclesMap_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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
rw : Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap (S.f ≫ S.g) i) 0
⊢ Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i)
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (opcyclesMap S.f i) (opcyclesMap S.g i)) 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap 0 i) 0
Tactic: rw [← opcyclesMap_comp, S.zero, opcyclesMap_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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
rw : Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap 0 i) 0
⊢ Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i)
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (opcyclesMap S.f i) (opcyclesMap S.g i)) 0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) 0 0
Tactic: rw [← opcyclesMap_comp, S.zero, opcyclesMap_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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
have dsimp : Epi (S.g.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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
      (opcyclesMap S.g i) ⋯).Exact
have this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
Tactic: have : Epi (ShortComplex.map S (eval C c i)).g := 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 : 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)))
⊢ (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
      (opcyclesMap S.g i) ⋯).Exact
have have : ∀
  (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))) sorry)),
  (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
      (opcyclesMap S.g i) sorry).Exact
Tactic: have hj := (hS.map (HomologicalComplex.eval C c i)).gIsCokernel
-- 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))) ⋯)
⊢ (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
      (opcyclesMap S.g i) ⋯).Exact
have hS₁ : IsColimit
  (CokernelCofork.ofπ
    (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
        (opcyclesMap S.g i) sorry).g
    sorry)
Tactic: apply ShortComplex.exact_of_g_is_cokernel
-- 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 :
  (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
        (opcyclesMap S.g i) ⋯).X₂ ⟶
    A
hk :
  (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
          (opcyclesMap S.g i) ⋯).f ≫
      k =
    0
⊢ { l :
    (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
          (opcyclesMap S.g i) ⋯).X₃ ⟶
      A //
    (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
            (opcyclesMap S.g i) ⋯).g ≫
        l =
      k }
have dsimp : { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = 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 : 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
⊢ ShortComplex.f (S.map (eval C c i)) ≫ S.X₂.pOpcycles i ≫ k = 0
have dsimp : S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 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 : 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
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0
have rw : CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) (opcyclesMap S.f i ≫ k) = 0
Tactic: rw [← p_opcyclesMap_assoc, hk, comp_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 : 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
rw : CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) (opcyclesMap S.f i ≫ k) = 0
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0
have rw₁ : Eq (α := S.X₁.X i ⟶ A) (CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) 0) 0
Tactic: rw [← p_opcyclesMap_assoc, hk, comp_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 : 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
rw : CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) (opcyclesMap S.f i ≫ k) = 0
rw₁ : Eq (α := S.X₁.X i ⟶ A) (CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) 0) 0
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁.X i ⟶ A) 0 0
Tactic: rw [← p_opcyclesMap_assoc, hk, comp_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 : 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
⊢ { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
have have : (H :
    { l :
      Cocone.pt (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))) sorry) ⟶
        A //
      Cofork.π (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) sorry) ≫ l = S.X₂.pOpcycles i ≫ k }) →
  { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
Tactic: have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_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 : 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 }
⊢ { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
have refine_1 : Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
Tactic: refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
-- 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.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
⊢ { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
have refine_2 : 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) =
  k
Tactic: refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
-- 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 }
⊢ 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)) (S.g.f (c.prev i) ≫ 0)
Tactic: rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]