awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
⊢ v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'
have pos : ∀ (hp : p' = p),
  v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: by_cases hp : p' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
pos :
  ∀ (hp : p' = p),
    v
        ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
          ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
              Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
            α))
        p' q' hpq' =
      α.v p' q' hpq'
⊢ v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'
have neg : ∀ (hp : ¬p' = p),
  v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: by_cases hp : p' = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X') K n) (fromSingleMk (g ≫ f) h)
    (comp (ofHom (CategoryTheory.Functor.map (singleFunctor C p) g)) (fromSingleMk f h) ⋯)
have a : Eq (α := X' ⟶ K.X q)
  ((fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X') K n) → X' ⟶ K.X q) (fromSingleMk (g ≫ f) h) :
    X' ⟶ K.X q)
  ((fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X') K n) → X' ⟶ K.X q)
      (comp (ofHom (CategoryTheory.Functor.map (singleFunctor C p) g)) (fromSingleMk f h) sorry) :
    X' ⟶ K.X q)
Tactic: apply (fromSingleEquiv h).injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
⊢ δ n n' (toSingleMk f h) =
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow (toSingleMk (K.d p' p ≫ f) h')
have pos : ∀ (hp : p' + 1 = p),
  δ n n' (toSingleMk f h) =
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow (toSingleMk (K.d p' p ≫ f) h')
Tactic: by_cases hp : p' + 1 = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
pos :
  ∀ (hp : p' + 1 = p),
    δ n n' (toSingleMk f h) =
      HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow (toSingleMk (K.d p' p ≫ f) h')
⊢ δ n n' (toSingleMk f h) =
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow (toSingleMk (K.d p' p ≫ f) h')
have neg : ∀ (hp : ¬p' + 1 = p),
  δ n n' (toSingleMk f h) =
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow (toSingleMk (K.d p' p ≫ f) h')
Tactic: by_cases hp : p' + 1 = p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ δ n n' (single (f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)) n) =
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow
      (single ((K.d p' p ≫ f) ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)) n')
have pos : single (q := q + 1)
      ((f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)) ≫
        HomologicalComplex.d (Functor.obj (singleFunctor C q) X) q (q + 1))
      n' +
    HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow
      (single (K.d p' p ≫ f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)) n') =
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n') n'.negOnePow
    (single ((K.d p' p ≫ f) ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)) n')
Tactic: rw [δ_single _ n n' (by lia) p' (q + 1) (by lia) rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K (Functor.obj (singleFunctor C q) X) n
⊢ (fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
      ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
          α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
        α) =
    α
have h₁ : ∀ (p' q' : ℤ) (hpq' : p' + n = q'),
  v
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
        ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
            α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: ext p' q' hpq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p' q' : ℤ
hpq' : p' + n = q'
⊢ v
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
        ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
            α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
          α))
      p' q' hpq' =
    α.v p' q' hpq'
have pos : ∀ (hq : q' = q),
  v
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
        ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
            α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: by_cases hq : q' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p' q' : ℤ
hpq' : p' + n = q'
pos :
  ∀ (hq : q' = q),
    v
        ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
          ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
              α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
            α))
        p' q' hpq' =
      α.v p' q' hpq'
⊢ v
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
        ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
            α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
          α))
      p' q' hpq' =
    α.v p' q' hpq'
have neg : ∀ (hq : ¬q' = q),
  v
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n))
        ((fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
            α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: by_cases hq : q' = q
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
X' : C
g : X ⟶ X'
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X') n) (toSingleMk (f ≫ g) h)
    (comp (toSingleMk f h) (ofHom (CategoryTheory.Functor.map (singleFunctor C q) g)) ⋯)
have a : Eq (α := K.X p ⟶ X')
  ((toSingleEquiv h : (a : Cochain K ((singleFunctor C q).obj X') n) → K.X p ⟶ X') (toSingleMk (f ≫ g) h) : K.X p ⟶ X')
  ((toSingleEquiv h : (a : Cochain K ((singleFunctor C q).obj X') n) → K.X p ⟶ X')
      (comp (toSingleMk f h) (ofHom (CategoryTheory.Functor.map (singleFunctor C q) g)) sorry) :
    K.X p ⟶ X')
Tactic: apply (toSingleEquiv h).injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (δ n (n + 1) (Cochain.fromSingleMk f h)) 0
have rw : Eq.{v + 1} (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk 0 sorry) 0
Tactic: rw [Cochain.δ_fromSingleMk _ _ _ q' (by lia), hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ Eq (α := Cocycle (Functor.obj (singleFunctor C p) X') K n) (fromSingleMk (g ≫ f) h q' hq' ⋯)
    (precomp (fromSingleMk f h q' hq' hf) (CategoryTheory.Functor.map (singleFunctor C p) g))
have h₁ : Eq (α := Cochain (Functor.obj (singleFunctor C p) X') K n)
  (↑(fromSingleMk (g ≫ f) h q' hq' sorry) : Cochain ((singleFunctor C p).obj X') K n)
  (↑(precomp (fromSingleMk f h q' hq' hf) (CategoryTheory.Functor.map (singleFunctor C p) g)) :
    Cochain ((singleFunctor C p).obj X') K n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
L : CochainComplex.{v, u, 0} C ℤ
g : K ⟶ L
⊢ Eq (α := Cocycle (Functor.obj (singleFunctor C p) X) L n) (fromSingleMk (f ≫ g.f q) h q' hq' ⋯)
    (postcomp (fromSingleMk f h q' hq' hf) g)
have h₁ : Eq (α := Cochain (Functor.obj (singleFunctor C p) X) L n)
  (↑(fromSingleMk (f ≫ g.f q) h q' hq' sorry) : Cochain ((singleFunctor C p).obj X) L n)
  (↑(postcomp (fromSingleMk f h q' hq' hf) g) : Cochain ((singleFunctor C p).obj X) L n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
⊢ ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
have obtain : ∀ (f : X ⟶ K.X q) (hf : Cochain.fromSingleMk f h = (↑α : Cochain ((singleFunctor C p).obj X) K n)),
  ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
Tactic: obtain ⟨f, hf⟩ := Cochain.fromSingleMk_surjective α.1 q h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = (↑α : Cochain ((singleFunctor C p).obj X) K n)
⊢ ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
have hα : Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1))
  (δ n (n + 1) (↑α : Cochain ((singleFunctor C p).obj X) K n)) 0
Tactic: have hα := α.δ_eq_zero (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = (↑α : Cochain ((singleFunctor C p).obj X) K n)
hα :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1))
    (δ n (n + 1) (↑α : Cochain ((singleFunctor C p).obj X) K n)) 0
⊢ ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
have hα₁ : Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk (f ≫ K.d q q') sorry) 0
Tactic: rw [← hf, Cochain.δ_fromSingleMk _ _ _ q' (by lia)] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = (↑α : Cochain ((singleFunctor C p).obj X) K n)
hα : Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk (f ≫ K.d q q') ⋯) 0
⊢ ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α
have hα₁ : Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C p) X) p ⟶ K.X q')
  (Cochain.v (Cochain.fromSingleMk (f ≫ K.d q q') sorry) p q' sorry) (Cochain.v 0 p q' sorry)
Tactic: replace hα := Cochain.congr_v hα p q' (by lia)
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = (↑α : Cochain ((singleFunctor C p).obj X) K n)
hα :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C p) X) p ⟶ K.X q')
    (Cochain.v (Cochain.fromSingleMk (f ≫ K.d q q') ⋯) p q' ⋯) (Cochain.v 0 p q' ⋯)
⊢ fromSingleMk f h q' hq' ⋯ = α
have h₁ : (↑(fromSingleMk f h q' hq' sorry) : Cochain ((singleFunctor C p).obj X) K n) =
  (↑α : Cochain ((singleFunctor C p).obj X) K n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
⊢ Membership.mem (γ := AddSubgroup (Cocycle (Functor.obj (singleFunctor C p) X) K n))
      (coboundaries (Functor.obj (singleFunctor C p) X) K n) (fromSingleMk f h q' hq' hf) ↔
    ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
have rw : (∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
    δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)) ↔
  ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
Tactic: rw [mem_coboundaries_iff _ (n - 1) (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
⊢ (∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
      δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)) ↔
    ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
have mp : (∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
    δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)) →
  ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
mp :
  (∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
      δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)) →
    ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
⊢ (∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
      δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)) ↔
    ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
have mpr : (∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f) →
  ∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
    δ (n - 1) n β = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
α : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)
hα : δ (n - 1) n α = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)
⊢ ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
have mp : ∀ (g : X ⟶ K.X q'') (hg : Cochain.fromSingleMk g sorry = α), ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
Tactic: obtain ⟨g, hg⟩ := Cochain.fromSingleMk_surjective α q'' (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
α : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)
hα : δ (n - 1) n α = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)
g : X ⟶ K.X q''
hg : Cochain.fromSingleMk g ⋯ = α
⊢ ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
have mp : g ≫ K.d q'' q = f
Tactic: refine ⟨g, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
α : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)
hα : δ (n - 1) n α = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)
g : X ⟶ K.X q''
hg : Cochain.fromSingleMk g ⋯ = α
⊢ g ≫ K.d q'' q = f
have hα₁ : Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (Cochain.fromSingleMk (g ≫ K.d q'' q) h)
  (Cochain.fromSingleMk f h)
Tactic: rw [← hg, fromSingleMk_coe, Cochain.δ_fromSingleMk _ _ _ _ h] at hα
Cleared hypotheses: hα, hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (δ n (n + 1) (Cochain.toSingleMk f h)) 0
have rw : HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (n + 1).negOnePow (Cochain.toSingleMk 0 sorry) = 0
Tactic: rw [Cochain.δ_toSingleMk _ _ _ p' (by lia), hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
X' : C
g : X ⟶ X'
⊢ Eq (α := Cocycle K (Functor.obj (singleFunctor C q) X') n) (toSingleMk (f ≫ g) h p' hp' ⋯)
    (postcomp (toSingleMk f h p' hp' hf) (CategoryTheory.Functor.map (singleFunctor C q) g))
have h₁ : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X') n)
  (↑(toSingleMk (f ≫ g) h p' hp' sorry) : Cochain K ((singleFunctor C q).obj X') n)
  (↑(postcomp (toSingleMk f h p' hp' hf) (CategoryTheory.Functor.map (singleFunctor C q) g)) :
    Cochain K ((singleFunctor C q).obj X') n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
L : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ K
⊢ Eq (α := Cocycle L (Functor.obj (singleFunctor C q) X) n) (toSingleMk (g.f p ≫ f) h p' hp' ⋯)
    (precomp (toSingleMk f h p' hp' hf) g)
have h₁ : Eq (α := Cochain L (Functor.obj (singleFunctor C q) X) n)
  (↑(toSingleMk (g.f p ≫ f) h p' hp' sorry) : Cochain L ((singleFunctor C q).obj X) n)
  (↑(precomp (toSingleMk f h p' hp' hf) g) : Cochain L ((singleFunctor C q).obj X) n)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
q n : ℤ
α : Cocycle K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
have obtain : ∀ (f : K.X p ⟶ X) (hf : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)),
  ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
Tactic: obtain ⟨f, hf⟩ := Cochain.toSingleMk_surjective α.1 p h