awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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)
g : X ⟶ K.X q''
hα :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (Cochain.fromSingleMk (g ≫ K.d q'' q) h)
    (Cochain.fromSingleMk f h)
hg : Cochain.fromSingleMk g ⋯ = α
⊢ g ≫ K.d q'' q = f

Tactic:
(Cochain.fromSingleEquiv h).symm.injective hα

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, AddEquiv.injective, AddEquiv.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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)
g : X ⟶ K.X q''
hα :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (Cochain.fromSingleMk (g ≫ K.d q'' q) h)
    (Cochain.fromSingleMk f h)
hg : Cochain.fromSingleMk g ⋯ = α
⊢ g ≫ K.d q'' q = f

Tactic:
exact (Cochain.fromSingleEquiv h).symm.injective hα

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, AddEquiv.injective, AddEquiv.symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
q' : ℤ
hq' : q + 1 = q'
q'' : ℤ
hq'' : q'' + 1 = q
g : X ⟶ K.X q''
hf : (g ≫ K.d q'' q) ≫ K.d q q' = 0
⊢ p + (n - 1) = q''

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
q' : ℤ
hq' : q + 1 = q'
q'' : ℤ
hq'' : q'' + 1 = q
g : X ⟶ K.X q''
hf : (g ≫ K.d q'' q) ≫ K.d q q' = 0
⊢ ∃ (β : Cochain (Functor.obj (singleFunctor C p) X) K (n - 1)),
    δ (n - 1) n β = (↑(fromSingleMk (g ≫ K.d q'' q) h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K n)

Tactic:
exact ⟨Cochain.fromSingleMk g (by lia), Cochain.δ_fromSingleMk _ _ _ _ h⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
⊢ p' + (n + 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
rw :
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (n + 1).negOnePow (Cochain.toSingleMk 0 ⋯) =
    0
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (δ n (n + 1) (Cochain.toSingleMk f h)) 0

Tactic:
rw [Cochain.δ_toSingleMk _ _ _ p' (by lia), hf]

Premises used: CochainComplex.HomComplex.Cochain.δ_toSingleMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
⊢ HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (n + 1).negOnePow (Cochain.toSingleMk 0 ⋯) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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'
⊢ K.d p' p ≫ f ≫ g = 0

Tactic:
simp [reassoc_of% hf]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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'
h₁ :
  Eq (α := Cochain K (Functor.obj (singleFunctor C q) X') n)
    (↑(toSingleMk (f ≫ g) h p' hp' ⋯) : 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)
⊢ 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))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 (α := K.X p ⟶ X')
    ((Cochain.toSingleEquiv h : (a : Cochain K ((singleFunctor C q).obj X') n) → K.X p ⟶ X')
        (↑(toSingleMk (f ≫ g) h p' hp' ⋯) : Cochain K ((singleFunctor C q).obj X') n) :
      K.X p ⟶ X')
    ((Cochain.toSingleEquiv h : (a : Cochain K ((singleFunctor C q).obj X') n) → K.X p ⟶ X')
        (↑(postcomp (toSingleMk f h p' hp' hf) (CategoryTheory.Functor.map (singleFunctor C q) g)) :
          Cochain K ((singleFunctor C q).obj X') n) :
      K.X p ⟶ X')

Tactic:
simp [Cochain.toSingleMk_postcomp]

Premises used: CochainComplex.HomComplex.Cochain.toSingleMk_postcomp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 (α := Cochain K (Functor.obj (singleFunctor C q) X') n)
    (↑(toSingleMk (f ≫ g) h p' hp' ⋯) : 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:
exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_postcomp])

Premises used: CochainComplex.HomComplex.Cochain.toSingleEquiv, AddEquiv.injective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
⊢ L.d p' p ≫ g.f p ≫ f = 0

Tactic:
simp [← g.comm_assoc, hf]

Premises used: HomologicalComplex.Hom.comm_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
h₁ :
  Eq (α := Cochain L (Functor.obj (singleFunctor C q) X) n)
    (↑(toSingleMk (g.f p ≫ f) h p' hp' ⋯) : Cochain L ((singleFunctor C q).obj X) n)
    (↑(precomp (toSingleMk f h p' hp' hf) g) : Cochain L ((singleFunctor C q).obj X) n)
⊢ 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)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 (α := L.X p ⟶ X)
    ((Cochain.toSingleEquiv h : (a : Cochain L ((singleFunctor C q).obj X) n) → L.X p ⟶ X)
        (↑(toSingleMk (g.f p ≫ f) h p' hp' ⋯) : Cochain L ((singleFunctor C q).obj X) n) :
      L.X p ⟶ X)
    ((Cochain.toSingleEquiv h : (a : Cochain L ((singleFunctor C q).obj X) n) → L.X p ⟶ X)
        (↑(precomp (toSingleMk f h p' hp' hf) g) : Cochain L ((singleFunctor C q).obj X) n) :
      L.X p ⟶ X)

Tactic:
simp [Cochain.toSingleMk_precomp]

Premises used: CochainComplex.HomComplex.Cochain.toSingleMk_precomp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 (α := Cochain L (Functor.obj (singleFunctor C q) X) n)
    (↑(toSingleMk (g.f p ≫ f) h p' hp' ⋯) : 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:
exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_precomp])

Premises used: CochainComplex.HomComplex.Cochain.toSingleEquiv, AddEquiv.injective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
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 = α
⊢ ∃ (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

Premises used: CochainComplex.HomComplex.Cochain.toSingleMk_surjective, Subtype.val
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1))
    (δ n (n + 1) (↑((n + 1).negOnePow • α) : Cochain K ((singleFunctor C q).obj X) n)) 0

Tactic:
have hα := ((n + 1).negOnePow • α).δ_eq_zero (n + 1)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα :
  HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (n + 1).negOnePow
      (δ n (n + 1) (Cochain.toSingleMk f h)) =
    0
⊢ p' + (n + 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα :
  Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1))
    (δ n (n + 1) (↑((n + 1).negOnePow • α) : Cochain K ((singleFunctor C q).obj X) n)) 0
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0

Tactic:
rw [coe_units_smul, δ_units_smul, ← hf, Cochain.δ_toSingleMk _ _ _ p' (by lia),
    smul_smul, Int.units_mul_self, one_smul] at hα

Premises used: CochainComplex.HomComplex.δ_units_smul, CochainComplex.HomComplex.Cocycle.coe_units_smul, smul_smul, one_smul, CochainComplex.HomComplex.Cochain.δ_toSingleMk, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
⟨f, ?_, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
refine_1 : K.d p' p ≫ f = 0
refine_2 : toSingleMk f h p' hp' ⋯ = α
⊢ ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
refine ⟨f, ?_, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ p' + (n + 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ K.d p' p ≫ f = 0

Tactic:
simpa [← cancel_mono (HomologicalComplex.singleObjXSelf (.up ℤ) q X).inv] using
    Cochain.congr_v hα p' q (by lia)

Premises used: CochainComplex.HomComplex.Cochain.congr_v, Int, CategoryTheory.cancel_mono, HomologicalComplex.singleObjXSelf, CategoryTheory.Iso.inv, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
refine_2 :
  (↑(toSingleMk f h p' hp' ⋯) : Cochain K ((singleFunctor C q).obj X) n) =
    (↑α : Cochain K ((singleFunctor C q).obj X) n)
⊢ toSingleMk f h p' hp' ⋯ = α

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 : Cochain.toSingleMk f h = (↑α : Cochain K ((singleFunctor C q).obj X) n)
hα : Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) (n + 1)) (Cochain.toSingleMk (K.d p' p ≫ f) ⋯) 0
⊢ (↑(toSingleMk f h p' hp' ⋯) : Cochain K ((singleFunctor C q).obj X) n) =
    (↑α : Cochain K ((singleFunctor C q).obj X) n)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 g : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
hg : K.d p' p ≫ g = 0
⊢ K.d p' p ≫ (f + g) = 0

Tactic:
simp [hf, hg]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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 g : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
hg : K.d p' p ≫ g = 0
⊢ K.d p' p ≫ (f - g) = 0

Tactic:
simp [hf, hg]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
⊢ K.d p' p ≫ (-f) = 0

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p' : ℤ
hp' : p' + 1 = p
⊢ Eq (α := K.X p' ⟶ X) (K.d p' p ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
⊢ n - 1 + 1 = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
rw :
  (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
⊢ Membership.mem (γ := AddSubgroup (Cocycle K (Functor.obj (singleFunctor C q) X) n))
      (coboundaries K (Functor.obj (singleFunctor C q) X) n) (toSingleMk f h p' hp' hf) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f

Tactic:
rw [mem_coboundaries_iff _ (n - 1) (by simp)]

Premises used: HSub.hSub, CochainComplex.HomComplex.mem_coboundaries_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
mp :
  (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) →
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
mpr :
  (∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f) →
    ∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
⊢ (∃ (β : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)),
      δ (n - 1) n β = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)) ↔
    ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
⊢ p'' + (n - 1) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
mp : ∀ (g : K.X p'' ⟶ X) (hg : Cochain.toSingleMk g ⋯ = α), ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f
⊢ ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f

Tactic:
obtain ⟨g, hg⟩ := Cochain.toSingleMk_surjective α p'' (by lia)

Premises used: CochainComplex.HomComplex.Cochain.toSingleMk_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
⊢ ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f

Tactic:
⟨n.negOnePow • g, ?_⟩

Premises used: Exists.intro, HSMul.hSMul, Int.negOnePow
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
mp : K.d p p'' ≫ (n.negOnePow • g) = f
⊢ ∃ (g : K.X p'' ⟶ X), K.d p p'' ≫ g = f

Tactic:
refine ⟨n.negOnePow • g, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
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
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K (Functor.obj (singleFunctor C q) X) (n - 1)
hα : δ (n - 1) n α = (↑(toSingleMk f h p' hp' hf) : Cochain K ((singleFunctor C q).obj X) n)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
⊢ HSMul.hSMul (β := Cochain K (Functor.obj (singleFunctor C q) X) n) n.negOnePow
      (Cochain.toSingleMk (K.d p p'' ≫ g) h) =
    Cochain.toSingleMk f h

Tactic:
rw [← hg, toSingleMk_coe, Cochain.δ_toSingleMk _ _ _ _ h] at hα

Premises used: CochainComplex.HomComplex.Cocycle.toSingleMk_coe, CochainComplex.HomComplex.Cochain.δ_toSingleMk