awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X Y : C
f : X ⟶ Y
obtain :
  ∀ (ha' : n + a = a + n),
    Eq (α :=
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
      (CategoryTheory.Functor.map
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            Y))
      (Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            X) ≫
        CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      (Functor.obj (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
      (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)

Tactic:
obtain rfl : a' = a + n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X Y : C
f : X ⟶ Y
ha' : n + a = a + n
hfg :
  Eq (α :=
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        a ⟶
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) Y) a)
    (Hom.f
      (CategoryTheory.Functor.map
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            Y))
      a)
    (Hom.f
      (Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            X) ≫
        CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
      a)
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X Y : C
f : X ⟶ Y
ha' : n + a = a + n
⊢ Eq (α :=
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        a ⟶
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) Y) a)
    (Hom.f
      (CategoryTheory.Functor.map
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            Y))
      a)
    (Hom.f
      (Iso.hom
          ((fun (X : C) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
                Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                  (Functor.obj
                    (single C (ComplexShape.up ℤ) (a + n) ⋙
                      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                    X)
                  (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
            X) ≫
        CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
      a)

Tactic:
simp [single]

Premises used: HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
a : ℤ
w :
  ∀ (x : C),
    Eq.{v + 1} (α :=
      X.{v, u, 0}
          (Functor.obj
            (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) x)
          a ⟶
        X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
      (Hom.f
        (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯))
          x)
        a)
      (Hom.f
        (NatTrans.app
          (Iso.hom
            (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a)
              (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)))
          x)
        a)
⊢ Eq (α :=
    Iso (C := C ⥤ CochainComplex.{v, u, 0} C ℤ)
      (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0)
      (single C (ComplexShape.up ℤ) a))
    (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
    (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a) (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
a : ℤ
x : C
w :
  Eq.{v + 1} (α :=
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) (a + 0) ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (eqToHom ⋯)
    (Hom.f
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ))
        (Functor.obj (single C (ComplexShape.up ℤ) a) x))
      a)
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a) (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)))
        x)
      a)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
a : ℤ
x : C
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) (a + 0) ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (eqToHom ⋯)
    (Hom.f
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ))
        (Functor.obj (single C (ComplexShape.up ℤ) a) x))
      a)

Tactic:
simp only [single, shiftFunctorZero_eq, shiftFunctorZero'_hom_app_f,
      XIsoOfEq, eqToIso.hom]

Premises used: CochainComplex.shiftFunctorZero_eq, CategoryTheory.eqToIso.hom, HomologicalComplex.XIsoOfEq, CochainComplex.shiftFunctorZero'_hom_app_f, HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
w :
  ∀ (x : C),
    Eq.{v + 1} (α :=
      X.{v, u, 0}
          (Functor.obj
            (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n)) x)
          a ⟶
        X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
      (Hom.f
        (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯))
          x)
        a)
      (Hom.f
        (NatTrans.app
          (Iso.hom
            (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'')
                (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
              Iso.symm
                  (Functor.associator (single C (ComplexShape.up ℤ) a'')
                    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
                    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
                Iso.trans (Y :=
                  single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  (Functor.isoWhiskerRight
                    (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
                    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
                  (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)))
          x)
        a)
⊢ Eq (α :=
    Iso (C := C ⥤ CochainComplex.{v, u, 0} C ℤ)
      (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n))
      (single C (ComplexShape.up ℤ) a))
    (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
    (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'') (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
      Iso.symm
          (Functor.associator (single C (ComplexShape.up ℤ) a'')
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
        Iso.trans (Y := single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
          (Functor.isoWhiskerRight
            (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
          (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : C
w :
  Eq.{v + 1} (α :=
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + (m + n)) ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (eqToHom ⋯)
    (Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n))
          (Functor.obj (single C (ComplexShape.up ℤ) a'') x))
        a ≫
      𝟙 (X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + n + m)) ≫ eqToHom ⋯ ≫ eqToHom ⋯)
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n)) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'')
              (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
            Iso.symm
                (Functor.associator (single C (ComplexShape.up ℤ) a'')
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
              Iso.trans (Y :=
                single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                (Functor.isoWhiskerRight
                  (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
                (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)))
        x)
      a)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : C
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + (m + n)) ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (eqToHom ⋯)
    (Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n))
          (Functor.obj (single C (ComplexShape.up ℤ) a'') x))
        a ≫
      𝟙 (X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + n + m)) ≫ eqToHom ⋯ ≫ eqToHom ⋯)

Tactic:
simp only [shiftFunctorAdd_eq, shiftFunctorAdd'_hom_app_f, XIsoOfEq,
      eqToIso.hom, eqToHom_trans, id_comp]

Premises used: CategoryTheory.eqToIso.hom, HomologicalComplex.XIsoOfEq, CochainComplex.shiftFunctorAdd_eq, CochainComplex.shiftFunctorAdd'_hom_app_f, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
⊢ Functor.Additive (D := CochainComplex.{v, u, 0} C ℤ) (single C (ComplexShape.up ℤ) n)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
R : Type u_1
inst_3 : Ring R
n : ℤ
inst_4 : Linear.{u_1, v, u} R C
X Y : C
f : X ⟶ Y
r : R
dsimp :
  { f := fun (i : ℤ) ↦ if h : i = n then eqToHom ⋯ ≫ (r • f) ≫ eqToHom ⋯ else 0, comm' := ⋯ } =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
        { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
        { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) })
      r
      { f := fun (i : ℤ) ↦ if h : i = n then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ :
        Hom
          { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
          { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) } }
⊢ CategoryTheory.Functor.map (SingleFunctors.functor (singleFunctors C) n) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) Y))
      r (CategoryTheory.Functor.map (SingleFunctors.functor (singleFunctors C) n) f)

Tactic:
dsimp [CochainComplex.singleFunctors, HomologicalComplex.single]

Premises used: CochainComplex.singleFunctors, HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
R : Type u_1
inst_3 : Ring R
n : ℤ
inst_4 : Linear.{u_1, v, u} R C
X Y : C
f : X ⟶ Y
r : R
⊢ { f := fun (i : ℤ) ↦ if h : i = n then eqToHom ⋯ ≫ (r • f) ≫ eqToHom ⋯ else 0, comm' := ⋯ } =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
        { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
        { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) })
      r
      { f := fun (i : ℤ) ↦ if h : i = n then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ :
        Hom
          { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
          { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) } }

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
n p q : ℤ
⊢ Eq.{v + 1} (α :=
    HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C n) X) p ⟶
      HomologicalComplex.X.{v, u, 0} (Functor.obj (singleFunctor C n) X) q)
    (d (Functor.obj (singleFunctor C n) X) p q) 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
⊢ Functor.Full (D := CochainComplex.{v, u, 0} C ℤ) (singleFunctor C n)

Tactic:
inferInstanceAs (single _ _ _).Full

Premises used: _private.0.CochainComplex.instFullIntSingleFunctor._proof_1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
⊢ Functor.Faithful (D := CochainComplex.{v, u, 0} C ℤ) (singleFunctor C n)

Tactic:
inferInstanceAs (single _ _ _).Faithful

Premises used: _private.0.CochainComplex.instFaithfulIntSingleFunctor._proof_1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
⊢ Functor.Additive (D := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (SingleFunctors.functor (CochainComplex.singleFunctors C) n ⋙ quotient C (ComplexShape.up ℤ))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
X : C
⊢ Eq (α := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (Functor.obj (quotient C (ComplexShape.up ℤ)) (Functor.obj (CochainComplex.singleFunctor C n) X))
    (Functor.obj (singleFunctor C n) X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
R : Type u_1
inst_3 : Ring R
inst_4 : Linear.{u_1, v, u} R C
n : ℤ
⊢ Functor.Linear R (D := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (singleFunctor C n)

Tactic:
inferInstanceAs (Functor.Linear R (CochainComplex.singleFunctor C n ⋙
    HomotopyCategory.quotient _ _))

Premises used: _private.0.HomotopyCategory.instLinearIntUpSingleFunctor._proof_1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ
f : w ⟶ w_1
g : w_1 ⟶ w_2
w_3 w_4 w_5 : CochainComplex.{v_1, u_1, 0} C ℤ
f' : w_3 ⟶ w_4
g' : w_4 ⟶ w_5
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
⊢ Eq (α :=
    CochainComplex.mappingCone g ⟶
      Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (CochainComplex.mappingConeCompTriangle f' g').obj₁)
    (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (CochainComplex.mappingConeCompTriangle f' g').mor₃ :
      CochainComplex.mappingCone g ⟶
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
          (CochainComplex.mappingConeCompTriangle f' g').obj₁)
    ((CochainComplex.mappingConeCompTriangle f g).mor₃ ≫
        CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
          (map f f' (φ.app 0) (φ.app 1) ⋯) :
      (CochainComplex.mappingConeCompTriangle f g).obj₃ ⟶
        Functor.obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (CochainComplex.mappingCone f'))

Tactic:
have eq := CochainComplex.mappingConeCompTriangle_mor₃_naturality f g f' g' φ