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 : CategoryTheory.Functor.{v, v', u, u'} C D
inst_4 : F.Additive
⊢ NatTrans.CommShift (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (D :=
    HomotopyCategory.{v', u', 0} D (ComplexShape.up ℤ)) (F₁ :=
    quotient C (ComplexShape.up ℤ) ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ))
    (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) ℤ

Tactic:
Quotient.liftCommShift_compatibility _ _ _ _

Premises used: CategoryTheory.Quotient.liftCommShift_compatibility, CategoryTheory.Functor.mapHomotopyCategory, HomotopyCategory, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (n.negOnePow • Iso.app (shiftEval C n i i' hi) K).hom ≫ (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K).f =
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          K).f ≫
      (Iso.app (shiftEval C n j j' hj) K).hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (Iso.app (shiftEval C n j j' hj) K).hom ≫ (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K).g =
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          K).g ≫
      (n.negOnePow • Iso.app (shiftEval C n k k' hk) K).hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          X).X₁ ⟶
      (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y).X₁)
    (ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            Y)))
    (ShortComplex.Hom.τ₁
      (Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            X) ≫
        CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          X).X₂ ⟶
      (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y).X₂)
    (ShortComplex.Hom.τ₂
      (CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            Y)))
    (ShortComplex.Hom.τ₂
      (Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            X) ≫
        CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k)
          X).X₃ ⟶
      (Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') Y).X₃)
    (ShortComplex.Hom.τ₃
      (CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            Y)))
    (ShortComplex.Hom.τ₃
      (Iso.hom
          ((fun (K : CochainComplex.{v_1, u_1, 0} C ℤ) ↦
              (ShortComplex.isoMk (n.negOnePow • Iso.app (shiftEval C n i i' hi) K) (Iso.app (shiftEval C n j j' hj) K)
                  (n.negOnePow • Iso.app (shiftEval C n k k' hk) K) ⋯ ⋯ :
                Functor.obj
                    (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n ⋙
                      shortComplexFunctor' C (up ℤ) i j k)
                    K ≅
                  Functor.obj (shortComplexFunctor' C (up ℤ) i' j' k') K))
            X) ≫
        CategoryTheory.Functor.map (shortComplexFunctor' C (up ℤ) i' j' k') f))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i i' : ℤ
hi : n + i = i'
simp : n + (i - 1) = i' - 1
⊢ n + (up ℤ).prev i = (up ℤ).prev i'

Tactic:
simp only [prev]

Premises used: CochainComplex.prev
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i i' : ℤ
hi : n + i = i'
⊢ n + (i - 1) = i' - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i i' : ℤ
hi : n + i = i'
simp : n + (i + 1) = i' + 1
⊢ n + (up ℤ).next i = (up ℤ).next i'

Tactic:
simp only [next]

Premises used: CochainComplex.next
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i i' : ℤ
hi : n + i = i'
⊢ n + (i + 1) = i' + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₁ =
    ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
h₂ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₂ =
    ShortComplex.Hom.τ₂
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
h₃ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₃ =
    ShortComplex.Hom.τ₃
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₁ =
    ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

Premises used: one_smul, CochainComplex.shiftFunctorZero_hom_app_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₂ =
    ShortComplex.Hom.τ₂
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

Premises used: one_smul, CochainComplex.shiftFunctorZero_hom_app_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₃ =
    ShortComplex.Hom.τ₃
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

Premises used: one_smul, CochainComplex.shiftFunctorZero_hom_app_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
rw₂ : mn + a = m + n + a
rw₃ rw₄ : mn + a = mn + a
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← add_assoc, hmn]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₁ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁
h₂ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₂ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₂
h₃ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₃ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₃
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  mn.negOnePow • (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
        ((up ℤ).prev a) ≫
      (n.negOnePow •
          (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₁ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₂ :
  (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) a ≫
      (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom ≫
        (XIsoOfEq K ⋯).hom
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₂ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₃ :
  mn.negOnePow • (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
        ((up ℤ).next a) ≫
      (n.negOnePow •
          (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₃ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
        ((up ℤ).prev a) ≫
      (n.negOnePow •
          (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

Tactic:
simp only [← hmn, Int.negOnePow_add, shiftFunctorAdd'_hom_app_f',
    XIsoOfEq_shift, Linear.comp_units_smul, Linear.units_smul_comp,
    XIsoOfEq_hom_comp_XIsoOfEq_hom, smul_smul]

Premises used: HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom, CategoryTheory.Linear.units_smul_comp, CochainComplex.XIsoOfEq_shift, smul_smul, Int.negOnePow_add, CategoryTheory.Linear.comp_units_smul, CochainComplex.shiftFunctorAdd'_hom_app_f'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) a ≫
      (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom ≫
        (XIsoOfEq K ⋯).hom

Tactic:
simp only [← hmn, Int.negOnePow_add, shiftFunctorAdd'_hom_app_f',
    XIsoOfEq_shift, Linear.comp_units_smul, Linear.units_smul_comp,
    XIsoOfEq_hom_comp_XIsoOfEq_hom, smul_smul]

Premises used: HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom, CategoryTheory.Linear.units_smul_comp, CochainComplex.XIsoOfEq_shift, smul_smul, Int.negOnePow_add, CategoryTheory.Linear.comp_units_smul, CochainComplex.shiftFunctorAdd'_hom_app_f'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
        ((up ℤ).next a) ≫
      (n.negOnePow •
          (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

Tactic:
simp only [← hmn, Int.negOnePow_add, shiftFunctorAdd'_hom_app_f',
    XIsoOfEq_shift, Linear.comp_units_smul, Linear.units_smul_comp,
    XIsoOfEq_hom_comp_XIsoOfEq_hom, smul_smul]

Premises used: HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom, CategoryTheory.Linear.units_smul_comp, CochainComplex.XIsoOfEq_shift, smul_smul, Int.negOnePow_add, CategoryTheory.Linear.comp_units_smul, CochainComplex.shiftFunctorAdd'_hom_app_f'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n ⋙ homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a') K)
    (NatTrans.app (Iso.hom (shiftIso C n a a' ha')) K)
    (ShortComplex.homologyMap (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha')) K))

Tactic:
simp [shiftIso, HomologicalComplex.homology]

Premises used: CochainComplex.ShiftSequence.shiftIso, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ Eq (α :=
    Functor.obj (homologyFunctor C (up ℤ) a') K ⟶
      Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n ⋙ homologyFunctor C (up ℤ) a) K)
    (NatTrans.app (Iso.inv (shiftIso C n a a' ha')) K)
    (ShortComplex.homologyMap (NatTrans.app (Iso.inv (shiftShortComplexFunctorIso C n a a' ha')) K))

Tactic:
simp [shiftIso, HomologicalComplex.homology]

Premises used: CochainComplex.ShiftSequence.shiftIso, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
a : ℤ
w :
  ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)),
    Eq (α :=
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
            homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a) K)
      (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a ⋯)) K)
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
              (homologyFunctor C (up ℤ) a) ≪≫
            Functor.leftUnitor (homologyFunctor C (up ℤ) a)))
        K)
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v_1, u_1, 0} C (up ℤ) ⥤ C)
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙ homologyFunctor C (up ℤ) a)
      (homologyFunctor C (up ℤ) a))
    (ShiftSequence.shiftIso C 0 a a ⋯)
    (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
        (homologyFunctor C (up ℤ) a) ≪≫
      Functor.leftUnitor (homologyFunctor C (up ℤ) a))

Tactic:
ext K