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 n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
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:
aesop
-- 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
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
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:
(HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_src
-- 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
α : Cochain (Functor.obj (singleFunctor C p) X) K n
p' q' : ℤ
hpq' : p' + n = q'
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:
exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_src
-- 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
f : X ⟶ K.X q
⊢ (fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
        Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n)) f) =
    f

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 n : ℤ
h : p + n = q
⊢ ∀ (x y : Cochain (Functor.obj (singleFunctor C p) X) K n),
    Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ (x + y).v p q h =
      Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ x.v p q h +
        Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ y.v p q h

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
⊢ (fromSingleEquiv h : (a : Cochain ((singleFunctor C p).obj X) K n) → X ⟶ K.X q) (fromSingleMk f h) = f

Tactic:
simp [fromSingleEquiv]

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv
-- 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
⊢ fromSingleMk (f + g) h =
    HAdd.hAdd (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (fromSingleMk f h) (fromSingleMk g h)

Tactic:
(fromSingleEquiv h).symm.map_add _ _

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, CochainComplex.HomComplex.Cochain.mk, dite, AddEquiv.map_add, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.fromSingleMk, 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 g : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ fromSingleMk (f - g) h =
    HSub.hSub (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (fromSingleMk f h) (fromSingleMk g h)

Tactic:
(fromSingleEquiv h).symm.map_sub _ _

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, CochainComplex.HomComplex.Cochain.mk, dite, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.fromSingleMk, AddEquiv.map_sub, 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
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n) (fromSingleMk (-f) h) (-fromSingleMk f h)

Tactic:
(fromSingleEquiv h).symm.map_neg _

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, CochainComplex.HomComplex.Cochain.mk, dite, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.fromSingleMk, AddEquiv.map_neg, 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 n : ℤ
α : Cochain (Functor.obj (singleFunctor C p) X) K n
q : ℤ
h : p + n = q
⊢ ∃ (f : X ⟶ K.X q), fromSingleMk f h = α

Tactic:
(fromSingleEquiv h).symm.surjective α

Premises used: CochainComplex.HomComplex.Cochain.fromSingleEquiv, CochainComplex.HomComplex.Cochain.mk, dite, AddEquiv.surjective, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.fromSingleMk, 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 ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
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) ⋯) :
      X' ⟶ K.X 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) ⋯)

Tactic:
apply (fromSingleEquiv h).injective

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

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

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

Tactic:
simp [fromSingleEquiv, singleFunctor, singleFunctors]

Premises used: CochainComplex.singleFunctor, CochainComplex.HomComplex.Cochain.fromSingleEquiv, CochainComplex.singleFunctors
-- 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
⊢ Eq.{v + 1} (α := Cochain K (Functor.obj (singleFunctor C q) X) n) (toSingleMk 0 h) 0

Tactic:
simp [toSingleMk]

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
⊢ Eq (α := K.X p ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C q) X) q) (v (toSingleMk f h) p q h)
    (f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))

Tactic:
simp [toSingleMk]

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' q' : ℤ
hpq' : p' + n = q'
hp' : p' ≠ p
⊢ Eq (α := K.X p' ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C q) X) q')
    (v (toSingleMk f h) p' q' hpq') 0

Tactic:
single_v_eq_zero _ _ _ _ _ hp'

Premises used: CochainComplex.HomComplex.Cochain.toSingleMk, CochainComplex.HomComplex.Cochain.single_v_eq_zero
-- 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
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')
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')
⊢ δ 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
-- 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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ n + 1 = n'

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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ p' + 1 = p

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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
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')
⊢ δ 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')

Tactic:
rw [δ_single _ n n' (by lia) p' (q + 1) (by lia) rfl]

Premises used: CochainComplex.HomComplex.Cochain.δ_single, HAdd.hAdd, OfNat.ofNat, rfl
-- 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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ 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:
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
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬n + 1 = n'

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
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬p' + 1 = p

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
n' p' : ℤ
h' : p' + n' = q
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:
simp [δ_shape n n' (by lia), HomologicalComplex.shape K p' p (by simp; lia)]

Premises used: CochainComplex.HomComplex.δ_shape, HomologicalComplex.shape
-- 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
α : Cochain K (Functor.obj (singleFunctor C q) X) n
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'
⊢ (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))
        α) =
    α

Tactic:
ext p' q' hpq'
-- 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
α : 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'
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'
⊢ 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
-- 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
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p' q' : ℤ
hpq' : p' + n = q'
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:
aesop
-- 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
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p' q' : ℤ
hpq' : p' + n = q'
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:
(HomologicalComplex.isZero_single_obj_X _ _ _ _ hq).eq_of_tgt _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p' q' : ℤ
hpq' : p' + n = q'
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:
exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hq).eq_of_tgt _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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
f : K.X p ⟶ X
⊢ (fun (α : Cochain K (Functor.obj (singleFunctor C q) X) n) ↦
        α.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X))
      ((fun (f : K.X p ⟶ X) ↦ (toSingleMk f h : Cochain K (Functor.obj (singleFunctor C q) X) n)) f) =
    f

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 n : ℤ
h : p + n = q
⊢ ∀ (x y : Cochain K (Functor.obj (singleFunctor C q) X) n),
    (x + y).v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X) =
      x.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X) +
        y.v p q h ≫ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X)

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
⊢ (toSingleEquiv h : (a : Cochain K ((singleFunctor C q).obj X) n) → K.X p ⟶ X) (toSingleMk f h) = f

Tactic:
simp [toSingleEquiv]

Premises used: 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 g : K.X p ⟶ X
n : ℤ
h : p + n = q
⊢ toSingleMk (f + g) h =
    HAdd.hAdd (α := Cochain K (Functor.obj (singleFunctor C q) X) n) (toSingleMk f h) (toSingleMk g h)

Tactic:
(toSingleEquiv h).symm.map_add _ _

Premises used: CochainComplex.HomComplex.Cochain.mk, dite, CochainComplex.HomComplex.Cochain.toSingleEquiv, AddEquiv.map_add, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.toSingleMk, 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 g : K.X p ⟶ X
n : ℤ
h : p + n = q
⊢ toSingleMk (f - g) h =
    HSub.hSub (α := Cochain K (Functor.obj (singleFunctor C q) X) n) (toSingleMk f h) (toSingleMk g h)

Tactic:
(toSingleEquiv h).symm.map_sub _ _

Premises used: CochainComplex.HomComplex.Cochain.mk, dite, CochainComplex.HomComplex.Cochain.toSingleEquiv, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.toSingleMk, AddEquiv.map_sub, 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 : K.X p ⟶ X
n : ℤ
h : p + n = q
⊢ Eq (α := Cochain K (Functor.obj (singleFunctor C q) X) n) (toSingleMk (-f) h) (-toSingleMk f h)

Tactic:
(toSingleEquiv h).symm.map_neg _

Premises used: CochainComplex.HomComplex.Cochain.mk, dite, CochainComplex.HomComplex.Cochain.toSingleEquiv, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.toSingleMk, AddEquiv.map_neg, 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 ℤ
q n : ℤ
α : Cochain K (Functor.obj (singleFunctor C q) X) n
p : ℤ
h : p + n = q
⊢ ∃ (f : K.X p ⟶ X), toSingleMk f h = α

Tactic:
(toSingleEquiv h).symm.surjective α

Premises used: CochainComplex.HomComplex.Cochain.mk, dite, AddEquiv.surjective, CochainComplex.HomComplex.Cochain.toSingleEquiv, CochainComplex.HomComplex.Cochain.single, CochainComplex.HomComplex.Cochain.toSingleMk, AddEquiv.symm