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 : K.X p ⟶ X
n : ℤ
h : p + n = q
X' : C
g : X ⟶ X'
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)) ⋯) :
      K.X p ⟶ 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)) ⋯)

Tactic:
apply (toSingleEquiv h).injective

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
X' : C
g : X ⟶ X'
⊢ 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)) ⋯) :
      K.X p ⟶ X')

Tactic:
simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]

Premises used: CochainComplex.singleFunctor, CochainComplex.singleFunctors, CochainComplex.HomComplex.Cochain.toSingleEquiv, HomologicalComplex.single_map_f_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 ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
L : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ K
⊢ Eq (α := L.X p ⟶ X)
    ((toSingleEquiv h : (a : Cochain L ((singleFunctor C q).obj X) n) → L.X p ⟶ X) (toSingleMk (g.f p ≫ f) h) :
      L.X p ⟶ X)
    ((toSingleEquiv h : (a : Cochain L ((singleFunctor C q).obj X) n) → L.X p ⟶ X) ((ofHom g).comp (toSingleMk f h) ⋯) :
      L.X p ⟶ X)

Tactic:
simp [toSingleEquiv, singleFunctor, singleFunctors]

Premises used: CochainComplex.singleFunctor, CochainComplex.singleFunctors, CochainComplex.HomComplex.Cochain.toSingleEquiv
-- 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
⊢ 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
rw : Eq.{v + 1} (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk 0 ⋯) 0
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (δ n (n + 1) (Cochain.fromSingleMk f h)) 0

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

Premises used: CochainComplex.HomComplex.Cochain.δ_fromSingleMk
-- 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
⊢ Eq.{v + 1} (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk 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 ℤ
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
⊢ (g ≫ f) ≫ K.d q q' = 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 ℤ
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
h₁ :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X') K n)
    (↑(fromSingleMk (g ≫ f) h q' hq' ⋯) : 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)
⊢ 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))

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 ℤ
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 (α := X' ⟶ K.X q)
    ((Cochain.fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X') K n) → X' ⟶ K.X q)
        (↑(fromSingleMk (g ≫ f) h q' hq' ⋯) : Cochain ((singleFunctor C p).obj X') K n) :
      X' ⟶ K.X q)
    ((Cochain.fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X') K n) → X' ⟶ K.X q)
        (↑(precomp (fromSingleMk f h q' hq' hf) (CategoryTheory.Functor.map (singleFunctor C p) g)) :
          Cochain ((singleFunctor C p).obj X') K n) :
      X' ⟶ K.X q)

Tactic:
simp [Cochain.fromSingleMk_precomp]

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk_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 ℤ
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 (α := Cochain (Functor.obj (singleFunctor C p) X') K n)
    (↑(fromSingleMk (g ≫ f) h q' hq' ⋯) : 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:
exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_precomp])

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, 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 : 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
⊢ (f ≫ g.f q) ≫ L.d q q' = 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 : 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
h₁ :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) L n)
    (↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) : Cochain ((singleFunctor C p).obj X) L n)
    (↑(postcomp (fromSingleMk f h q' hq' hf) g) : Cochain ((singleFunctor C p).obj X) L n)
⊢ 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)

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 : 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 (α := X ⟶ L.X q)
    ((Cochain.fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X) L n) → X ⟶ L.X q)
        (↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) : Cochain ((singleFunctor C p).obj X) L n) :
      X ⟶ L.X q)
    ((Cochain.fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X) L n) → X ⟶ L.X q)
        (↑(postcomp (fromSingleMk f h q' hq' hf) g) : Cochain ((singleFunctor C p).obj X) L n) :
      X ⟶ L.X q)

Tactic:
simp [Cochain.fromSingleMk_postcomp]

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk_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 : 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 (α := Cochain (Functor.obj (singleFunctor C p) X) L n)
    (↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) : 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:
exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_postcomp])

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, 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 n : ℤ
α : Cocycle (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
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 = α
⊢ ∃ (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

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk_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 ℤ
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)
⊢ 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)
-- 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 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.fromSingleMk 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 ℤ
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
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K (n + 1)) (Cochain.fromSingleMk (f ≫ K.d q q') ⋯) 0

Tactic:
rw [← hf, Cochain.δ_fromSingleMk _ _ _ q' (by lia)] at hα

Premises used: CochainComplex.HomComplex.Cochain.δ_fromSingleMk
-- 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 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
⊢ 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 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
⊢ 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' ⋯)

Tactic:
replace hα := Cochain.congr_v hα p q' (by 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 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' ⋯)
⊢ f ≫ K.d q q' = 0

Tactic:
simpa using 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 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' ⋯)
h₁ :
  (↑(fromSingleMk f h q' hq' ⋯) : Cochain ((singleFunctor C p).obj X) K n) =
    (↑α : Cochain ((singleFunctor C p).obj X) K n)
⊢ fromSingleMk f h q' hq' ⋯ = α

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 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' ⋯) : Cochain ((singleFunctor C p).obj X) K n) =
    (↑α : Cochain ((singleFunctor C p).obj X) K 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 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' ⋯)
⊢ ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α

Tactic:
exact ⟨f, by simpa using hα, by ext : 1; 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
hg : g ≫ K.d q q' = 0
⊢ (f + g) ≫ K.d q q' = 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
hg : g ≫ K.d q q' = 0
⊢ (f - g) ≫ K.d q q' = 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ (-f) ≫ K.d q q' = 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
q' : ℤ
hq' : q + 1 = q'
⊢ Eq (α := X ⟶ K.X q') (0 ≫ K.d q q') 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 : 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
⊢ 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 : 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
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
⊢ 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

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 : 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
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)
⊢ (∃ (β : 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
-- 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)
hα : δ (n - 1) n α = (↑(fromSingleMk f h q' hq' hf) : Cochain ((singleFunctor C p).obj X) K 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 : 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)
mp : ∀ (g : X ⟶ K.X q'') (hg : Cochain.fromSingleMk g ⋯ = α), ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f
⊢ ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f

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

Premises used: CochainComplex.HomComplex.Cochain.fromSingleMk_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 : 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

Tactic:
⟨g, ?_⟩

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 ℤ
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 ⋯ = α
mp : g ≫ K.d q'' q = f
⊢ ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f

Tactic:
refine ⟨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 : 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 ⋯ = α
⊢ 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α

Premises used: CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CochainComplex.HomComplex.Cocycle.fromSingleMk_coe
-- 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)
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 ⋯ = α
hα₁ :
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (Cochain.fromSingleMk (g ≫ K.d q'' q) h)
    (Cochain.fromSingleMk f h)
⊢ Cochain.fromSingleMk g ⋯ = α

Tactic:
rw [← hg, fromSingleMk_coe, Cochain.δ_fromSingleMk _ _ _ _ h] at hα

Premises used: CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CochainComplex.HomComplex.Cocycle.fromSingleMk_coe