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
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
h₁ :
  ∀ (i : ℤ),
    Eq (α := (Functor.obj (shiftFunctor C n₁₂) X).X i ⟶ (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) Y).X i)
      (Hom.f
        (CategoryTheory.Functor.map (shiftFunctor C n₁₂) f ≫
          Iso.hom
            ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
                (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
                  Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
              Y))
        i)
      (Hom.f
        (Iso.hom
            ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
                (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
                  Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
              X) ≫
          CategoryTheory.Functor.map (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) f)
        i)
⊢ Eq (α := Functor.obj (shiftFunctor C n₁₂) X ⟶ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) Y)
    (CategoryTheory.Functor.map (shiftFunctor C n₁₂) f ≫
      Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
              Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
          Y))
    (Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
              Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
          X) ≫
      CategoryTheory.Functor.map (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) f)

Tactic:
ext
-- 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₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
i : ℤ
⊢ Eq (α := (Functor.obj (shiftFunctor C n₁₂) X).X i ⟶ (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) Y).X i)
    (Hom.f
      (CategoryTheory.Functor.map (shiftFunctor C n₁₂) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
                Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
            Y))
      i)
    (Hom.f
      (Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
                Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
            X) ≫
        CategoryTheory.Functor.map (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) f)
      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
n : ℤ
⊢ Functor.Additive (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n)

Tactic:
inferInstanceAs <| (CochainComplex.shiftFunctor C n).Additive

Premises used: _private.0.CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor._proof_1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n p : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) K).X p = K.X (p + 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
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
n p : ℤ
⊢ Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) K).X p ⟶
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L).X p)
    (Hom.f (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) φ) p)
    (φ.f (p + 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
K : CochainComplex.{v, u, 0} C ℤ
n i j : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) K).d i j =
    HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ K.X (j + { as := n : Discrete ℤ }.as)) n.negOnePow
      (K.d (i + { as := n : Discrete ℤ }.as) (j + { as := n : Discrete ℤ }.as))

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 : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
dsimp : n + b + a = n + (a + b)
⊢ n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as = n + { as := a + b : Discrete ℤ }.as

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 : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : n + b + a = n + (b + a)
rw₁ rw₂ : n + (b + a) = n + (b + a)
⊢ n + b + a = n + (a + b)

Tactic:
rw [add_comm a, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ Hom.f (NatTrans.app (Iso.inv (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, Int.add, 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 : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
dsimp : n + (a + b) = n + b + a
⊢ n + { as := a + b : Discrete ℤ }.as = n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as

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 : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : n + (b + a) = n + b + a
rw₁ rw₂ : n + (b + a) = n + (b + a)
⊢ n + (a + b) = n + b + a

Tactic:
rw [add_comm a, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom

Tactic:
tauto
-- 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 : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
dsimp : n + b + a = n + ab
⊢ n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as = n + { as := ab : Discrete ℤ }.as

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 : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + b + a = n + (a + b)
rw₁ : n + (b + a) = n + (a + b)
rw₂ rw₃ : n + (b + a) = n + (b + a)
⊢ n + b + a = n + ab

Tactic:
rw [← h, add_assoc, add_comm a]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
subst :
  Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b ab h)) K) n =
    (XIsoOfEq K ⋯).hom

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : Hom.f (NatTrans.app (Iso.inv (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom
rw₁ rw₂ : (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]

Premises used: CochainComplex.shiftFunctorAdd_inv_app_f, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- 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 : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
dsimp : n + ab = n + b + a
⊢ n + { as := ab : Discrete ℤ }.as = n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as

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 : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + (a + b) = n + b + a
rw₁ : n + (a + b) = n + (b + a)
rw₂ rw₃ : n + (b + a) = n + (b + a)
⊢ n + ab = n + b + a

Tactic:
rw [← h, add_assoc, add_comm a]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
subst :
  Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b ab h)) K) n =
    (XIsoOfEq K ⋯).hom

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom
rw₁ rw₂ : (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]

Premises used: CochainComplex.shiftFunctorAdd_hom_app_f, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
rw rw₁ : n = n
⊢ n = n + 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Hom.f (NatTrans.app (Iso.inv (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) K) n = (XIsoOfEq K ⋯).hom

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, Int.add, 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
rw rw₁ : n = n
⊢ n + 0 = n

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) K) n = (XIsoOfEq K ⋯).hom

Tactic:
tauto
-- 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 : CochainComplex.{v, u, 0} C ℤ
n p q : ℤ
hpq : p = q
rw rw₁ : q + n = q + n
⊢ p + n = q + n

Tactic:
rw [hpq]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n p q : ℤ
hpq : p = q
⊢ XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) K) hpq = XIsoOfEq K ⋯

Tactic:
rfl

Premises used: HomologicalComplex.XIsoOfEq, Int.add, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b c : ℤ
h : a + b = c
w :
  ∀ (x : CochainComplex.{v, u, 0} C ℤ) (i : ℤ),
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b c h)) x) i =
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b c h)) x).f i
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) c)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b c h) (shiftFunctorAdd' C a b c h)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b c : ℤ
h : a + b = c
x : CochainComplex.{v, u, 0} C ℤ
i : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b c h)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b c h)) x).f i

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

Premises used: CategoryTheory.eqToIso.hom, HomologicalComplex.XIsoOfEq, CochainComplex.shiftFunctorAdd'_hom_app_f', CochainComplex.shiftFunctorAdd'_hom_app_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b : ℤ
rw :
  Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯) (shiftFunctorAdd' C a b (a + b) ⋯)
rw₁ rw₂ :
  Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (shiftFunctorAdd' C a b (a + b) ⋯) (shiftFunctorAdd' C a b (a + b) ⋯)
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b) (shiftFunctorAdd' C a b (a + b) ⋯)

Tactic:
rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]

Premises used: CochainComplex.shiftFunctorAdd'_eq, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
w :
  ∀ (x : CochainComplex.{v, u, 0} C ℤ) (i : ℤ),
    Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) x) i =
      (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) (𝟭 (CochainComplex.{v, u, 0} C ℤ)))
    (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ) (shiftFunctorZero' C 0 ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
x : CochainComplex.{v, u, 0} C ℤ
i : ℤ
w : (XIsoOfEq x ⋯).hom = (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i
w₁ w₂ : (XIsoOfEq x ⋯).hom = (XIsoOfEq x ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i

Tactic:
rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]

Premises used: CochainComplex.shiftFunctorZero'_hom_app_f, CochainComplex.shiftFunctorZero_hom_app_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
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
rw : p + (b + a) = p + a + b
rw₁ : p + (a + b) = p + a + b
rw₂ rw₃ : p + (a + b) = p + (a + b)
⊢ p + b + a = p + a + b

Tactic:
rw [add_assoc, add_comm b, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
rw :
  Hom.f
      (NatTrans.app
        (Iso.hom
          (Iso.symm (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯) ≪≫
            CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯))
        K)
      p =
    Iso.hom (XIsoOfEq K ⋯)
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v, u, 0} C ℤ) a b)) K) p = Iso.hom (XIsoOfEq K ⋯)

Tactic:
rw [shiftFunctorComm_eq _ _ _ _ rfl]

Premises used: CategoryTheory.shiftFunctorComm_eq, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
dsimp :
  Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) p ≫
      Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯)) K)
        p =
    Iso.hom (XIsoOfEq K ⋯)
⊢ Hom.f
      (NatTrans.app
        (Iso.hom
          (Iso.symm (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯) ≪≫
            CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯))
        K)
      p =
    Iso.hom (XIsoOfEq K ⋯)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
rw : (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = Iso.hom (XIsoOfEq K ⋯)
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) p ≫
      Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯)) K)
        p =
    Iso.hom (XIsoOfEq K ⋯)

Tactic:
rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']

Premises used: CochainComplex.shiftFunctorAdd'_inv_app_f', CochainComplex.shiftFunctorAdd'_hom_app_f'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
⊢ (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom = Iso.hom (XIsoOfEq K ⋯)

Tactic:
simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans]

Premises used: CategoryTheory.eqToIso.hom, HomologicalComplex.XIsoOfEq, 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
n i i' : ℤ
hi : n + i = i'
K : CochainComplex.{v, u, 0} C ℤ
dsimp : i + n = i'
⊢ i + { as := n : Discrete ℤ }.as = 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
n i i' : ℤ
hi : n + i = i'
K : CochainComplex.{v, u, 0} C ℤ
rw : i + n = n + i
rw₁ rw₂ : n + i = n + i
⊢ i + n = i'

Tactic:
rw [← hi, add_comm i]

Premises used: add_comm
-- 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 i i' : ℤ
hi : n + i = i'
⊢ ∀ {X Y : CochainComplex.{v, u, 0} C ℤ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ eval C (ComplexShape.up ℤ) i) X ⟶
        Functor.obj (eval C (ComplexShape.up ℤ) i') Y)
      (CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ eval C (ComplexShape.up ℤ) i) f ≫
        Iso.hom ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦ XIsoOfEq K ⋯) Y))
      (Iso.hom ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦ XIsoOfEq K ⋯) X) ≫
        CategoryTheory.Functor.map (eval C (ComplexShape.up ℤ) i') f)

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
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
x : X ⟶ Y
i : ℤ
h : F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = F.map (x.f (i + n))
h₁ h₂ : Eq (α := F.obj (X.X (i + n)) ⟶ F.obj (Y.X (i + n))) (F.map (x.f (i + n))) (F.map (x.f (i + n)))
⊢ F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = 𝟙 (F.obj (X.X (i + n))) ≫ F.map (x.f (i + n))

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp