awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
have rw : (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.toCycles (𝟙 i) f f sorry n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
Tactic: rw [← cancel_epi (X.cyclesIsoH f n₁ n₂ hn₂).inv,
    cyclesIsoH_inv .., cyclesIsoH_inv_hom_id_assoc ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ Iso.inv
      (ShortComplex.LeftHomologyData.homologyIso
        (ShortComplex.HomologyData.left (X.homologyDataIdId f (n₁ - 1) n₁ n₂ ⋯ ⋯))) =
    X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
have rw : Iso.inv h.cyclesIso ≫ (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).homologyπ =
  h.π ≫ X.toCycles (𝟙 i) f f sorry n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
Tactic: rw [← cancel_epi h.π, h.π_comp_homologyIso_inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
have rw : h.right.p = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f sorry)
Tactic: rw [← cancel_epi (X.opcyclesIso ..).inv, Iso.inv_hom_id_assoc,
      ← cancel_epi (X.pOpcycles ..), p_opcyclesIso_inv_assoc ..,
      h.right.pOpcycles_comp_opcyclesIso_hom, p_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ h.right.p = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
have dsimp : 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f sorry)
Tactic: dsimp [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
have rw : (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f sorry)
Tactic: rw [← Functor.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 j) f ⋯)
have e_a : 𝟙 (mk₁ f) = twoδ₂Toδ₁ f (𝟙 j) f sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
⊢ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂
have this : Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f sorry n₁
Tactic: have : h.right.opcyclesIso.hom =
      (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫
        X.fromOpcycles f (𝟙 j) f (by simp) n₁ := by
    rw [← cancel_epi (X.opcyclesIso ..).inv, Iso.inv_hom_id_assoc,
      ← cancel_epi (X.pOpcycles ..), p_opcyclesIso_inv_assoc ..,
      h.right.pOpcycles_comp_opcyclesIso_hom, p_fromOpcycles]
    dsimp [h]
    rw [← Functor.map_id]
    congr 1
    cat_disch
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂
this : Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂
have obtain : ∀ (hn₂ : n₁ + 1 = n₁ + 1),
  let h := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂;
  ∀
    (this :
      Iso.hom h.right.opcyclesIso =
        (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f sorry n₁),
    (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv =
      X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂
Tactic: obtain rfl : n₂ = n₁ + 1 := by lia
Cleared hypotheses: n₂, hn₂, h, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂
have rw : (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
  X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f sorry n₁
Tactic: rw [← cancel_mono (X.opcyclesIsoH f n₀ n₁ hn₁).hom, Category.assoc,
    opcyclesIsoH_hom .., opcyclesIsoH_inv_hom_id ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
have dsimp : Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
  (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f))
    (Iso.hom
        (ShortComplex.LeftHomologyData.homologyIso
          (ShortComplex.HomologyData.left (X.homologyDataIdId f n₀ n₁ (n₁ + 1) sorry sorry))) :
      X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (𝟙 ((X.H n₁).obj (mk₁ f))))
  (((X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫
      (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom) ≫
    X.fromOpcycles f (𝟙 j) f sorry n₁)
Tactic: dsimp [EIsoH, ιE]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  Iso.hom h.right.opcyclesIso = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f))
      (Iso.hom
          (ShortComplex.LeftHomologyData.homologyIso
            (ShortComplex.HomologyData.left (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯))) :
        X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
      (𝟙 ((X.H n₁).obj (mk₁ f))))
    (((X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫
        (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom) ≫
      X.fromOpcycles f (𝟙 j) f ⋯ n₁)
have rw : Eq (α := X.E (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ⟶ (X.H n₁).obj (mk₁ f))
  (Iso.hom (h.right.homologyIso ≪≫ h.iso.symm) ≫ 𝟙 ((X.H n₁).obj (mk₁ f))) (Iso.hom h.right.homologyIso ≫ h.right.ι)
Tactic: rw [Category.assoc, ← this,
    h.left_homologyIso_eq_right_homologyIso_trans_iso_symm,
    ← ShortComplex.RightHomologyData.homologyIso_hom_comp_ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫
      X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ =
    0
have rw : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
Tactic: rw [← cancel_epi (X.pOpcycles ..), comp_zero,
    p_opcyclesMap_assoc _ _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
have dsimp : Mono (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
have rw : ∀ (P : C) (g : P ⟶ X.opcycles f₁ f₂₃ n₁),
  g ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0 → g = 0
Tactic: rw [Preadditive.mono_iff_cancel_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx : x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ = 0
⊢ x = 0
have hx₁ : (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) sorry n₁ =
  0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) sorry n₁
Tactic: replace hx := hx =≫ X.fromOpcycles f₁₂ f₃ _ rfl n₁
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁
⊢ x = 0
have hx₁ : x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) sorry n₁ = 0
Tactic: rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx :
  (x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁) ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ =
    0 ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁
hx₁ :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
⊢ x = 0
have hx₂ : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) sorry n₁) 0
Tactic: rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx_1 :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁) 0
⊢ x = 0
have rw : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) sorry n₁)
  (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) sorry n₁)
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx_1 :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁) 0
rw :
  Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
⊢ x = 0
have rw₁ : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) 0 (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) sorry n₁)
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x : A ⟶ X.opcycles f₁ f₂₃ n₁
hx_1 :
  x ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫ X.fromOpcycles f₁₂ f₃ (f₁₂ ≫ f₃) ⋯ n₁ = 0
hx : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁) 0
rw :
  Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) (x ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
    (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
rw₁ : Eq (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) 0 (0 ≫ X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) ⋯ n₁)
⊢ x = 0
have rw₂ : Eq.{v_1 + 1} (α := A ⟶ (X.H n₁).obj (mk₁ (f₁₂ ≫ f₃))) 0 0
Tactic: rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g
have dsimp : Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f =
    (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f ≫
      𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂
have dsimp : X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
  ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)
have rw : X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
  (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁
Tactic: rw [Category.comp_id, X.p_opcyclesMap _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁
⊢ X.pOpcycles f₁ f₂₃ n₁ ≫ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ =
    ((X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁) ≫ 𝟙 (X.opcycles f₁₂ f₃ n₁)
have rw₁ : (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ sorry) ≫ X.pOpcycles f₁₂ f₃ n₁ =
  (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) ≫ X.pOpcycles f₁₂ f₃ n₁
Tactic: rw [Category.comp_id, X.p_opcyclesMap _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
φ : X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯ ⟶
  X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ ⋯ ⋯ :=
  { τ₁ := X.pOpcycles f₁ f₂₃ n₁, τ₂ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₂,
    τ₃ := 𝟙 (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact
have rw : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ sorry sorry).Exact
Tactic: rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]