awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
this : (functor (F.lift G Φ hΦ) a ⋙ G).Additive
⊢ (functor (F.lift G Φ hΦ) a).Additive

Tactic:
Functor.additive_of_comp_faithful _ G

Premises used: CategoryTheory.Functor.additive_of_comp_faithful
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
this : (functor (F.lift G Φ hΦ) a ⋙ G).Additive
⊢ (functor (F.lift G Φ hΦ) a).Additive

Tactic:
exact Functor.additive_of_comp_faithful _ G

Premises used: CategoryTheory.Functor.additive_of_comp_faithful
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a : A
⊢ t.z a 0 = 1

Tactic:
simpa using t.assoc a 0 0

Premises used: CategoryTheory.TwistShiftData.assoc, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
b : A
⊢ t.z 0 b = 1

Tactic:
simpa using t.assoc 0 0 b

Premises used: CategoryTheory.TwistShiftData.assoc, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : C
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C c) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C c) X)
    (Functor.map (shiftFunctor C c) ((↑(t.z a b) : CatCenter C).app X))
    ((↑(t.z a b) : CatCenter C).app (Functor.obj.{v, v, u, u} (shiftFunctor C c) X))

Tactic:
simpa using NatTrans.shift_app_comm (t.z a b).val c X

Premises used: Units.val, CategoryTheory.NatTrans.shift_app_comm, CategoryTheory.TwistShiftData.z
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b : A
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C b) Y)
      (Functor.map (shiftFunctor C (a + b)) f ≫
        Iso.hom
          ((fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C b) X)
                (t.z a b) (Iso.app (shiftFunctorAdd C a b) X))
            Y))
      (Iso.hom
          ((fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C b) X)
                (t.z a b) (Iso.app (shiftFunctorAdd C a b) X))
            X) ≫
        Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) f)

Tactic:
simp [CatCenter.naturality_assoc, CatCenter.naturality, CatCenter.smul_iso_hom_eq]

Premises used: CategoryTheory.CatCenter.naturality_assoc, CategoryTheory.CatCenter.naturality, CategoryTheory.CatCenter.smul_iso_hom_eq
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
dsimp :
  (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X))
          (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X)).hom ≫
      Functor.map (shiftFunctor C c)
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a b) (Iso.app (shiftFunctorAdd C a b) X)).hom =
    eqToHom ⋯ ≫
      (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X)).hom ≫
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X) ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
            (t.z b c) (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))).hom
⊢ NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor C (a + b) ⋙ shiftFunctor C c) X)
                (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X))
            ⋯))
        X ≫
      Functor.map (shiftFunctor C c)
        ((NatIso.ofComponents
                (fun (X : C) ↦
                  HSMul.hSMul (β :=
                    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
                      Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C b) X)
                    (t.z a b) (Iso.app (shiftFunctorAdd C a b) X))
                ⋯).hom.app
          X) =
    eqToHom ⋯ ≫
      NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (X : C) ↦
                HSMul.hSMul (β :=
                  Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
                    Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C (b + c)) X)
                  (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X))
              ⋯))
          X ≫
        (NatIso.ofComponents
                (fun (X : C) ↦
                  HSMul.hSMul (β :=
                    Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) X ≅
                      Functor.obj.{v, v, u, u} (shiftFunctor C b ⋙ shiftFunctor C c) X)
                    (t.z b c) (Iso.app (shiftFunctorAdd C b c) X))
                ⋯).hom.app
          (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
simp :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
    (Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
      (↑(t.z (a + b) c) : CatCenter t.Category).app
          (Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X)) ≫
        Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
          Functor.map (shiftFunctor C c)
            ((↑(t.z a b) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
    (eqToHom ⋯ ≫
      Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
        (↑(t.z a (b + c)) : CatCenter t.Category).app
            (Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
            (↑(t.z b c) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
⊢ (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X))
          (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X)).hom ≫
      Functor.map (shiftFunctor C c)
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a b) (Iso.app (shiftFunctorAdd C a b) X)).hom =
    eqToHom ⋯ ≫
      (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X)).hom ≫
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X) ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
            (t.z b c) (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))).hom

Tactic:
simp only [Functor.map_comp, Category.assoc, CatCenter.smul_iso_hom_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.CatCenter.smul_iso_hom_eq
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
rw :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
    ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
      Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
        Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)))
    ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
      eqToHom ⋯ ≫
        Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
          Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
    (Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
      (↑(t.z (a + b) c) : CatCenter t.Category).app
          (Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X)) ≫
        Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
          Functor.map (shiftFunctor C c)
            ((↑(t.z a b) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
    (eqToHom ⋯ ≫
      Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
        (↑(t.z a (b + c)) : CatCenter t.Category).app
            (Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
            (↑(t.z b c) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))

Tactic:
rw [CatCenter.naturality, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      CatCenter.naturality_assoc, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      t.shift_z_app, CatCenter.naturality, CatCenter.naturality_assoc,
      ← CatCenter.mul_app_assoc, ← CatCenter.mul_app_assoc,
      ← Units.val_mul, ← Units.val_mul, t.assoc a b c]

Premises used: CategoryTheory.CatCenter.naturality_assoc, CategoryTheory.CatCenter.naturality, CategoryTheory.TwistShiftData.assoc, CategoryTheory.TwistShiftData.shift_z_app, CategoryTheory.CatCenter.mul_app_assoc, Units.val_mul
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
    ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
      Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
        Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)))
    ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
      eqToHom ⋯ ≫
        Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
          Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))

Tactic:
simp [shiftFunctorAdd_assoc_hom_app (C := C) a b c X, shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.shiftFunctorAdd_assoc_hom_app
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
⊢ ∀ (n : A) (X : t.Category),
    NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (0 + n)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} C (A := A) 0 ⋙ shiftFunctor C n) X)
                (t.z 0 n) (Iso.app (shiftFunctorAdd C 0 n) X))
            ⋯))
        X =
      eqToHom ⋯ ≫ Functor.map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)

Tactic:
simp [shiftFunctorAdd_zero_add_hom_app, CatCenter.smul_iso_hom_eq]

Premises used: CategoryTheory.shiftFunctorAdd_zero_add_hom_app, CategoryTheory.CatCenter.smul_iso_hom_eq
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
⊢ ∀ (n : A) (X : t.Category),
    NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (n + 0)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor.{v, u, w} C (A := A) 0) X)
                (t.z n 0) (Iso.app (shiftFunctorAdd C n 0) X))
            ⋯))
        X =
      eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Functor.obj.{v, v, u, u} (shiftFunctor C n) X)

Tactic:
simp [shiftFunctorAdd_add_zero_hom_app, CatCenter.smul_iso_hom_eq]

Premises used: CategoryTheory.shiftFunctorAdd_add_zero_hom_app, CategoryTheory.CatCenter.smul_iso_hom_eq
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
X Y : t.Category
f : X ⟶ Y
m : A
⊢ Functor.map (shiftFunctor t.Category m) f =
    (t.shiftIso m).hom.app X ≫ Functor.map (shiftFunctor C m) f ≫ (t.shiftIso m).inv.app Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
X : t.Category
⊢ NatTrans.app (Iso.hom (shiftFunctorZero t.Category A)) X =
    NatTrans.app (Iso.hom (t.shiftIso 0)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X

Tactic:
(Category.id_comp _).symm

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.shiftFunctor, CategoryTheory.TwistShiftData.instCategoryCategory._aux_3, Eq.symm, CategoryTheory.TwistShiftData.Category, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
X : t.Category
⊢ NatTrans.app (Iso.inv (shiftFunctorZero t.Category A)) X =
    NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.inv (t.shiftIso 0)) X

Tactic:
(Category.comp_id _).symm

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.shiftFunctor, CategoryTheory.Category.comp_id, CategoryTheory.TwistShiftData.instCategoryCategory._aux_3, Eq.symm, CategoryTheory.TwistShiftData.Category
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
dsimp :
  NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd t.Category i j)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X))
      (↑(t.z i j) : CatCenter C) (NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C i j)) X)
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)

Tactic:
dsimp [shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd'
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)

Tactic:
have : (shiftFunctorAdd' t.Category i j k h).hom.app X =
      (t.z i j).val • (shiftFunctorAdd' C i j k h).hom.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
rw :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
e_a :
  NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso k).hom.app X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
          (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
⊢ HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
e_a :
  NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
          𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso k).hom.app X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
          (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)

Tactic:
change _ = 𝟙 _ ≫ _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ 𝟙 _

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map