awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
w :
  𝟙 (F.obj (x.X (i + 0))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) i) ≫
      HomologicalComplex.Hom.f
        (NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
          (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i
⊢ Eq (α :=
    HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          x)
        i ⟶
      HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
          x)
        i)
    (HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso 0)) x) i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
    (HomologicalComplex.Hom.f
        (map (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) ≫
          NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
            (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
⊢ 𝟙 (F.obj (x.X (i + 0))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) i) ≫
      HomologicalComplex.Hom.f
        (NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
          (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i

Tactic:
simp only [CochainComplex.shiftFunctorZero_inv_app_f, CochainComplex.shiftFunctorZero_hom_app_f,
       HomologicalComplex.XIsoOfEq, eqToIso, eqToHom_map, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_map, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.eqToIso, HomologicalComplex.XIsoOfEq, CategoryTheory.eqToHom_refl, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
a b : ℤ
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
w :
  𝟙 (F.obj (x.X (i + (a + b)))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) i) ≫
      HomologicalComplex.Hom.f
        (NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
          (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i
⊢ 𝟙 (F.obj (x.X (i + (a + b)))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) i) ≫
      𝟙 (F.obj (x.X (i + b + a))) ≫
        𝟙 (F.obj (x.X (i + b + a))) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
              (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
            i

Tactic:
rw [id_comp, id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
a b : ℤ
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
⊢ 𝟙 (F.obj (x.X (i + (a + b)))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) i) ≫
      HomologicalComplex.Hom.f
        (NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
          (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i

Tactic:
simp only [CochainComplex.shiftFunctorAdd_hom_app_f,
      CochainComplex.shiftFunctorAdd_inv_app_f, HomologicalComplex.XIsoOfEq, eqToIso,
      eqToHom_map, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToIso, HomologicalComplex.XIsoOfEq, CategoryTheory.eqToHom_refl, CochainComplex.shiftFunctorAdd_inv_app_f, CochainComplex.shiftFunctorAdd_hom_app_f, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
n : ℤ
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
      (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
        F.mapHomologicalComplex (ComplexShape.up ℤ))
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n))
    (commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n :
      Iso (C :=
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n))
    (F.mapCochainComplexShiftIso n :
      Iso (C :=
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) ⥤ HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
          F.mapHomologicalComplex (ComplexShape.up ℤ))
        (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
          shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
K : CochainComplex.{v, u, 0} C ℤ
n i : ℤ
⊢ HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n)) K) i =
    𝟙
      (HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          K)
        i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
K : CochainComplex.{v, u, 0} C ℤ
n i : ℤ
⊢ HomologicalComplex.Hom.f (NatTrans.app (Iso.inv (commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n)) K) i =
    𝟙
      (HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) n)
          K)
        i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
dsimp : HSMul.hSMul (β := K.X (i + n) ⟶ L.X (j + n)) n.negOnePow (h.hom (i + n) (j + n)) = 0
⊢ HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ L.X (j + { as := n : Discrete ℤ }.as)) n.negOnePow
      (h.hom (i + { as := n : Discrete ℤ }.as) (j + { as := n : Discrete ℤ }.as)) =
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
a : ¬(ComplexShape.up ℤ).Rel (j + n) (i + n)
⊢ HSMul.hSMul (β := K.X (i + n) ⟶ L.X (j + n)) n.negOnePow (h.hom (i + n) (j + n)) = 0

Tactic:
rw [h.zero, smul_zero]

Premises used: smul_zero, Homotopy.zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬j + 1 = i
hij' : j + n + 1 = i + n
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ (ComplexShape.up ℤ).Rel i (i + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ (ComplexShape.up ℤ).Rel (i - 1) i

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
dsimp :
  φ₁.f (i + n) =
    HSMul.hSMul (β := K.X (i + n) ⟶ K.X (i + 1 + n)) n.negOnePow (K.d (i + n) (i + 1 + n)) ≫
          HSMul.hSMul (β := K.X (i + 1 + n) ⟶ L.X (i + n)) n.negOnePow (h.hom (i + 1 + n) (i + n)) +
        HSMul.hSMul (β := K.X (i + n) ⟶ L.X (i - 1 + n)) n.negOnePow (h.hom (i + n) (i - 1 + n)) ≫
          HSMul.hSMul (β := L.X (i - 1 + n) ⟶ L.X (i + n)) n.negOnePow (L.d (i - 1 + n) (i + n)) +
      φ₂.f (i + n)
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₁) i =
    (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).d i (i + 1) ≫
          HSMul.hSMul (β := K.X (i + 1 + { as := n : Discrete ℤ }.as) ⟶ L.X (i + { as := n : Discrete ℤ }.as))
            n.negOnePow (h.hom (i + 1 + { as := n : Discrete ℤ }.as) (i + { as := n : Discrete ℤ }.as)) +
        HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ L.X (i - 1 + { as := n : Discrete ℤ }.as)) n.negOnePow
            (h.hom (i + { as := n : Discrete ℤ }.as) (i - 1 + { as := n : Discrete ℤ }.as)) ≫
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).d (i - 1) i +
      HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₂) i

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ i + n + 1 = i + 1 + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ i - 1 + n + 1 = i + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ φ₁.f (i + n) =
    HSMul.hSMul (β := K.X (i + n) ⟶ K.X (i + 1 + n)) n.negOnePow (K.d (i + n) (i + 1 + n)) ≫
          HSMul.hSMul (β := K.X (i + 1 + n) ⟶ L.X (i + n)) n.negOnePow (h.hom (i + 1 + n) (i + n)) +
        HSMul.hSMul (β := K.X (i + n) ⟶ L.X (i - 1 + n)) n.negOnePow (h.hom (i + n) (i - 1 + n)) ≫
          HSMul.hSMul (β := L.X (i - 1 + n) ⟶ L.X (i + n)) n.negOnePow (L.d (i - 1 + n) (i + n)) +
      φ₂.f (i + n)

Tactic:
simpa only [Linear.units_smul_comp, Linear.comp_units_smul, smul_smul,
      Int.units_mul_self, one_smul,
      dNext_eq _ (show (ComplexShape.up ℤ).Rel (i + n) (i + 1 + n) by dsimp; lia),
      prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1 + n) (i + n) by dsimp; lia)]
        using h.comm (i + n)

Premises used: CategoryTheory.Linear.units_smul_comp, smul_smul, prevD_eq, CategoryTheory.Linear.comp_units_smul, one_smul, HAdd.hAdd, Homotopy.comm, dNext_eq, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
⊢ HomRel.IsCompatibleWithShift (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (homotopic C (ComplexShape.up ℤ)) ℤ

Tactic:
⟨fun n _ _ _ _ ⟨h⟩ => ⟨h.shift n⟩⟩

Premises used: HomRel.IsCompatibleWithShift.mk, CategoryTheory.shiftFunctor, HomologicalComplex, Int, Nonempty.intro, CategoryTheory.Functor.map, _private.0.HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic.match_1, homotopic, Homotopy.shift, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
⊢ HasShift
    (CategoryTheory.Quotient (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
      (homotopic C (ComplexShape.up ℤ)))
    ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
n : ℤ
⊢ Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (Functor.obj (quotient C (ComplexShape.up ℤ)) K) =
    Functor.obj (quotient C (ComplexShape.up ℤ))
      (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K)

Tactic:
Quotient.functor_obj_shift ..

Premises used: CategoryTheory.Quotient.functor_obj_shift, HomotopyCategory
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
⊢ Functor.Additive (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)

Tactic:
have : ((quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor _ n)).Additive :=
    Functor.additive_of_iso ((quotient C (ComplexShape.up ℤ)).commShiftIso n)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
this :
  Functor.Additive (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
⊢ Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)

Tactic:
apply Functor.additive_of_full_essSurj_comp (quotient _ _)

Premises used: HomotopyCategory.quotient, CategoryTheory.Functor.additive_of_full_essSurj_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
f :
  Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
r : R
obtain :
  ∀ (f : X ⟶ Y),
    CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        (HSMul.hSMul (β :=
          Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
          r
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f :
            Functor.obj (quotient C (ComplexShape.up ℤ)) X ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) Y)) =
      HSMul.hSMul (β :=
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
        r
        (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) :
          Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
            (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
              (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
            (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
              (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
⊢ CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) f)

Tactic:
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective f

Premises used: Int, HomotopyCategory.quotient, rfl, ComplexShape.up, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
      Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        Y)
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
        X)
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)) f ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map
      (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) f)

Tactic:
have h₁ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
      Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        Y)
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
        X)
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)) f ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map
      (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) f)
⊢ Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
      Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
        Y)
    (CategoryStruct.comp (Y :=
      Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
        X)
      (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
      (CategoryTheory.Functor.map
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
          (r • f) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
    (CategoryTheory.Functor.map
      (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f))

Tactic:
have h₂ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) (r • f)