awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
X X' : A
w :
  ∀ (x : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X : Discrete A })
              (obj (Discrete.functor h.F) { as := X' : Discrete A })).obj
          x ⟶
        (obj (Discrete.functor h.F)
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X : Discrete A }
                { as := X' : Discrete A })).obj
          x)
      (NatTrans.app
        (MonoidalCategoryStruct.whiskerRight
            (map (Discrete.functor h.F)
              { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
                ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) })
            (obj (Discrete.functor h.F) { as := X' : Discrete A }) ≫
          Iso.hom (Iso.symm (h.add { as := X }.as { as := X' }.as)))
        x)
      (NatTrans.app
        (Iso.hom (Iso.symm (h.add { as := X : Discrete A }.as { as := X' : Discrete A }.as)) ≫
          map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerRight { down := { down := ⋯ } } { as := X' }))
        x)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X : Discrete A })
        (obj (Discrete.functor h.F) { as := X' : Discrete A }) ⟶
      obj (Discrete.functor h.F)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X : Discrete A } { as := X' : Discrete A }))
    (MonoidalCategoryStruct.whiskerRight
        (map (Discrete.functor h.F)
          { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
            ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) })
        (obj (Discrete.functor h.F) { as := X' : Discrete A }) ≫
      Iso.hom (Iso.symm (h.add { as := X }.as { as := X' }.as)))
    (Iso.hom (Iso.symm (h.add { as := X : Discrete A }.as { as := X' : Discrete A }.as)) ≫
      map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerRight { down := { down := ⋯ } } { as := X' }))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
X X' : A
x : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X : Discrete A })
            (obj (Discrete.functor h.F) { as := X' : Discrete A })).obj
        x ⟶
      (obj (Discrete.functor h.F)
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X : Discrete A }
              { as := X' : Discrete A })).obj
        x)
    (NatTrans.app
      (MonoidalCategoryStruct.whiskerRight
          (map (Discrete.functor h.F)
            { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
              ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) })
          (obj (Discrete.functor h.F) { as := X' : Discrete A }) ≫
        Iso.hom (Iso.symm (h.add { as := X }.as { as := X' }.as)))
      x)
    (NatTrans.app
      (Iso.hom (Iso.symm (h.add { as := X : Discrete A }.as { as := X' : Discrete A }.as)) ≫
        map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerRight { down := { down := ⋯ } } { as := X' }))
      x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
X X' : A
w :
  ∀ (x : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X' : Discrete A })
              (obj (Discrete.functor h.F) { as := X : Discrete A })).obj
          x ⟶
        (obj (Discrete.functor h.F)
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X' : Discrete A }
                { as := X : Discrete A })).obj
          x)
      (NatTrans.app
        (MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := X' : Discrete A })
            (map (Discrete.functor h.F)
              { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
                ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) }) ≫
          Iso.hom (Iso.symm (h.add { as := X' }.as { as := X }.as)))
        x)
      (NatTrans.app
        (Iso.hom (Iso.symm (h.add { as := X' : Discrete A }.as { as := X : Discrete A }.as)) ≫
          map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerLeft { as := X' } { down := { down := ⋯ } }))
        x)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X' : Discrete A })
        (obj (Discrete.functor h.F) { as := X : Discrete A }) ⟶
      obj (Discrete.functor h.F)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X' : Discrete A } { as := X : Discrete A }))
    (MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := X' : Discrete A })
        (map (Discrete.functor h.F)
          { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
            ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) }) ≫
      Iso.hom (Iso.symm (h.add { as := X' }.as { as := X }.as)))
    (Iso.hom (Iso.symm (h.add { as := X' : Discrete A }.as { as := X : Discrete A }.as)) ≫
      map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerLeft { as := X' } { down := { down := ⋯ } }))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
X X' : A
x : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := X' : Discrete A })
            (obj (Discrete.functor h.F) { as := X : Discrete A })).obj
        x ⟶
      (obj (Discrete.functor h.F)
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := X' : Discrete A }
              { as := X : Discrete A })).obj
        x)
    (NatTrans.app
      (MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := X' : Discrete A })
          (map (Discrete.functor h.F)
            { down := { down := ⋯ : PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as) } :
              ULift.{u_1, 0} (PLift ({ as := X : Discrete A }.as = { as := X : Discrete A }.as)) }) ≫
        Iso.hom (Iso.symm (h.add { as := X' }.as { as := X }.as)))
      x)
    (NatTrans.app
      (Iso.hom (Iso.symm (h.add { as := X' : Discrete A }.as { as := X : Discrete A }.as)) ≫
        map (Discrete.functor h.F) (MonoidalCategoryStruct.whiskerLeft { as := X' } { down := { down := ⋯ } }))
      x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
              (obj (Discrete.functor h.F) { as := m₂ : Discrete A }))
            (obj (Discrete.functor h.F) { as := m₃ : Discrete A })).obj
        X ⟶
      (obj (Discrete.functor h.F)
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ : Discrete A }
                { as := m₃ : Discrete A }))).obj
        X)
    (NatTrans.app
      (MonoidalCategoryStruct.whiskerRight
          (Iso.hom (Iso.symm (h.add { as := m₁ : Discrete A }.as { as := m₂ : Discrete A }.as)))
          (obj (Discrete.functor h.F) { as := m₃ : Discrete A }) ≫
        Iso.hom
            (Iso.symm
              (h.add
                (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
                    { as := m₂ : Discrete A }).as
                { as := m₃ : Discrete A }.as)) ≫
          map (Discrete.functor h.F)
            (Iso.hom (MonoidalCategoryStruct.associator { as := m₁ } { as := m₂ } { as := m₃ })))
      X)
    (NatTrans.app
      (Iso.hom
          (MonoidalCategoryStruct.associator (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
            (obj (Discrete.functor h.F) { as := m₂ : Discrete A })
            (obj (Discrete.functor h.F) { as := m₃ : Discrete A })) ≫
        MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
            (Iso.hom (Iso.symm (h.add { as := m₂ : Discrete A }.as { as := m₃ : Discrete A }.as))) ≫
          Iso.hom
            (Iso.symm
              (h.add { as := m₁ }.as
                (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ } { as := m₃ }).as)))
      X)

Tactic:
simp [h.assoc_inv_app_assoc]

Premises used: CategoryTheory.ShiftMkCore.assoc_inv_app_assoc
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
w :
  ∀ (X : C),
    NatTrans.app (Iso.hom (MonoidalCategoryStruct.leftUnitor (obj (Discrete.functor h.F) { as := n : Discrete A }))) X =
      NatTrans.app
        (MonoidalCategoryStruct.whiskerRight h.zero.symm.hom (obj (Discrete.functor h.F) { as := n : Discrete A }) ≫
          Iso.hom
              (Iso.symm
                (h.add (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
                  { as := n : Discrete A }.as)) ≫
            map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.leftUnitor { as := n : Discrete A })))
        X
⊢ Iso.hom (MonoidalCategoryStruct.leftUnitor (obj (Discrete.functor h.F) { as := n : Discrete A })) =
    MonoidalCategoryStruct.whiskerRight h.zero.symm.hom (obj (Discrete.functor h.F) { as := n : Discrete A }) ≫
      Iso.hom
          (Iso.symm
            (h.add (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
              { as := n : Discrete A }.as)) ≫
        map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.leftUnitor { as := n : Discrete A }))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ NatTrans.app (Iso.hom (MonoidalCategoryStruct.leftUnitor (obj (Discrete.functor h.F) { as := n : Discrete A }))) X =
    NatTrans.app
      (MonoidalCategoryStruct.whiskerRight h.zero.symm.hom (obj (Discrete.functor h.F) { as := n : Discrete A }) ≫
        Iso.hom
            (Iso.symm
              (h.add (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
                { as := n : Discrete A }.as)) ≫
          map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.leftUnitor { as := n : Discrete A })))
      X

Tactic:
simp [h.zero_add_inv_app, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.ShiftMkCore.zero_add_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
w :
  ∀ (X : C),
    NatTrans.app (Iso.hom (MonoidalCategoryStruct.rightUnitor (obj (Discrete.functor h.F) { as := n : Discrete A })))
        X =
      NatTrans.app
        (MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := n : Discrete A }) h.zero.symm.hom ≫
          Iso.hom
              (Iso.symm
                (h.add { as := n : Discrete A }.as
                  (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))) ≫
            map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.rightUnitor { as := n : Discrete A })))
        X
⊢ Iso.hom (MonoidalCategoryStruct.rightUnitor (obj (Discrete.functor h.F) { as := n : Discrete A })) =
    MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := n : Discrete A }) h.zero.symm.hom ≫
      Iso.hom
          (Iso.symm
            (h.add { as := n : Discrete A }.as
              (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))) ≫
        map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.rightUnitor { as := n : Discrete A }))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ NatTrans.app (Iso.hom (MonoidalCategoryStruct.rightUnitor (obj (Discrete.functor h.F) { as := n : Discrete A }))) X =
    NatTrans.app
      (MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := n : Discrete A }) h.zero.symm.hom ≫
        Iso.hom
            (Iso.symm
              (h.add { as := n : Discrete A }.as
                (Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))) ≫
          map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.rightUnitor { as := n : Discrete A })))
      X

Tactic:
simp [h.add_zero_inv_app]

Premises used: CategoryTheory.ShiftMkCore.add_zero_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j k : A
h : i + j = k
rw rw₁ : Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C k) (shiftFunctor C k)
⊢ Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C k) (shiftFunctor C (i + j))

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
w :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C (i + j)) (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.hom (shiftFunctorAdd' C i j (i + j) ⋯)) (Iso.hom (shiftFunctorAdd C i j))
⊢ Eq (α := Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C (i + j)) (shiftFunctor C i ⋙ shiftFunctor C j))
    (shiftFunctorAdd' C i j (i + j) ⋯) (shiftFunctorAdd C i j)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C (i + j)) (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.hom (shiftFunctorAdd' C i j (i + j) ⋯)) (Iso.hom (shiftFunctorAdd C i j))

Tactic:
apply Category.id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
ha : a = 0
rw rw₁ :
  Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor.{v, u, u_1} C (A := A) 0) (shiftFunctor.{v, u, u_1} C (A := A) 0)
⊢ Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C a) (shiftFunctor.{v, u, u_1} C (A := A) 0)

Tactic:
rw [ha]
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
a : A
⊢ shiftFunctor C a = h.F a

Tactic:
rfl

Premises used: CategoryTheory.shiftFunctor, rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
⊢ shiftFunctorZero C A = h.zero

Tactic:
rfl

Premises used: CategoryTheory.shiftFunctorZero, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
a b : A
⊢ shiftFunctorAdd C a b = h.add a b

Tactic:
rfl

Premises used: CategoryTheory.shiftFunctorAdd, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
w :
  ∀ (X : C),
    Eq.{v + 1} (α :=
      obj.{v, v, u, u} (shiftFunctor C a) X ⟶
        obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a) X)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 a a ⋯)) X)
      (NatTrans.app
        (Iso.hom
          (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
            isoWhiskerRight (Iso.symm (shiftFunctorZero C A)) (shiftFunctor C a)))
        X)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C a) (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a))
    (shiftFunctorAdd' C 0 a a ⋯)
    (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫ isoWhiskerRight (Iso.symm (shiftFunctorZero C A)) (shiftFunctor C a))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
w :
  Eq (α :=
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 a)) X :
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (𝟙 (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X) ≫
        map (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A)) X) :
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 a a ⋯)) X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorZero C A)) (shiftFunctor C a)))
      X)

Tactic:
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorZero, CategoryTheory.shiftFunctorAdd'
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
w :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 a)) X)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A)
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)) { as := a : Discrete A }))
        X)
      (eqToHom ⋯)
      (NatTrans.app
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)) { as := a })
        X))
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 a)) X :
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (𝟙 (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X) ≫
        map (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A)) X) :
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))

Tactic:
simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.Discrete.addMonoidal_leftUnitor, CategoryTheory.obj_ε_app, CategoryTheory.eqToIso.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 : Discrete A }) X))
    (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C 0 a)) X)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A)
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)) { as := a : Discrete A }))
        X)
      (eqToHom ⋯)
      (NatTrans.app
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)) { as := a })
        X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
w :
  ∀ (x : C),
    Eq.{v + 1} (α :=
      obj.{v, v, u, u} (shiftFunctor C a) x ⟶
        obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) x)
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C a 0 a ⋯)) x)
      (NatTrans.app
        (Iso.hom
          (Iso.symm (rightUnitor (shiftFunctor C a)) ≪≫
            isoWhiskerLeft (shiftFunctor C a) (Iso.symm (shiftFunctorZero C A))))
        x)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C a) (shiftFunctor C a ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0))
    (shiftFunctorAdd' C a 0 a ⋯)
    (Iso.symm (rightUnitor (shiftFunctor C a)) ≪≫ isoWhiskerLeft (shiftFunctor C a) (Iso.symm (shiftFunctorZero C A)))

Tactic:
ext