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
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 := 0 })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))
    (NatTrans.app (eqToHom ⋯) x ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a 0)) 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 := 0 })
          (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 }) x) ≫
        NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A))
          (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 }) x ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))
⊢ 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)

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 := 0 })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))
    (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a 0)) x)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a : Discrete A }
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))
        x)
      (eqToHom ⋯)
      (NatTrans.app
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a }
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory 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 := 0 })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))
    (NatTrans.app (eqToHom ⋯) x ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a 0)) 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 := 0 })
          (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 }) x) ≫
        NatTrans.app (LaxMonoidal.ε (shiftMonoidalFunctor C A))
          (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 }) x ⟶
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := 0 })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))

Tactic:
simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.Discrete.addMonoidal_rightUnitor, CategoryTheory.ε_app_obj, 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 := 0 })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a : Discrete A }) x))
    (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a 0)) x)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u}
        (obj (shiftMonoidalFunctor C A)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a : Discrete A }
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))
        x)
      (eqToHom ⋯)
      (NatTrans.app
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a }
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory 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₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ rw : a₁ + a₂ + a₃ = a₁₂₃
rw₁ rw₂ : a₁₂₃ = a₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
rw [← h₁₂, 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
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
rw : a₁ + (a₂ + a₃) = a₁₂₃
rw₁ : a₁ + a₂ + a₃ = a₁₂₃
rw₂ rw₃ : a₁₂₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

Premises used: add_assoc
-- 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₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
subst :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C (a₁ + a₂ + a₃))
      (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃))
    (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
        associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯))
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C a₁₂₃)
      (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (shiftFunctor C a₃) ≪≫
        associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃))

Tactic:
subst h₁₂ h₂₃ 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
a₁ a₂ a₃ : A
w :
  ∀ (X : C),
    Eq.{v + 1} (α :=
      obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
        obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃) X)
      (NatTrans.app
        (Iso.hom
          (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
              associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)))
        X)
      (NatTrans.app
        (Iso.hom
          (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)))
        X)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C (a₁ + a₂ + a₃))
      (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃))
    (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
        associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + 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₂ a₃ : A
X : C
w :
  NatTrans.app (Iso.hom (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯)) X) ≫
        𝟙
          (obj.{v, v, u, u} (shiftFunctor C a₃)
            (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X))) =
    NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C a₁) X)
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃) X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
          isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
            associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)))
      X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)))
      X)

Tactic:
dsimp
-- 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₂ a₃ : A
X : C
w :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯)) X) ≫
        𝟙
          (obj.{v, v, u, u} (shiftFunctor C a₃)
            (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X))) =
    NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C a₁) X)

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.shiftFunctorAdd'_eq_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₂ a₃ : A
X : C
w :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    ((NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))

Tactic:
dsimp [shiftFunctorAdd']

Premises used: 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₂ a₃ : A
X : C
w :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    ((eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    ((NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))

Tactic:
simp only [eqToHom_app]

Premises used: CategoryTheory.eqToHom_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
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + 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 := a₂ : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X)))
    (eqToHom ⋯ ≫
      NatTrans.app
          (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₂ } { as := a₃ }))
          X ≫
        NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ : Discrete A } { as := a₃ : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ + a₃ : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))
        (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }) X :
          obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + (a₂ + a₃) : Discrete A }) X ⟶
            obj.{v, v, u, u}
              (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A } ⋙
                obj (shiftMonoidalFunctor C A) { as := a₂ + a₃ : Discrete A })
              X)
        (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ })
            (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₂ + a₃ : Discrete A })
              (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 (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
              (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete 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₂ a₃ : A
w :
  ∀ (X : C),
    Eq.{v + 1} (α :=
      obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
        obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃) X)
      (NatTrans.app
        (Iso.hom
          (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
            isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
              associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)))
        X)
      (NatTrans.app
        (Iso.hom
          (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)))
        X)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C (a₁ + a₂ + a₃))
      (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃))
    (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ 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
⊢ 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)
    (map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_zero_add C a)) X

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.hom
-- 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
dsimp : obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) (obj.{v, v, u, u} (𝟭 C) X)

Tactic:
dsimp
-- 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
rw rw₁ : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) X

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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} (shiftFunctor C (0 + 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)) X)
    (eqToHom ⋯ ≫ map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))

Tactic:
simp [← shiftFunctorAdd'_zero_add_hom_app, shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.shiftFunctorAdd'_zero_add_hom_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
a : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 a a ⋯)) X)
    (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_zero_add C a)) X

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.inv
-- 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
dsimp : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (0 + a)) X
⊢ obj.{v, v, u, u} (shiftFunctor C a) (obj.{v, v, u, u} (𝟭 C) X) = obj.{v, v, u, u} (shiftFunctor C (0 + a)) X

Tactic:
dsimp
-- 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
rw rw₁ : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (0 + a)) X

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a) X ⟶
      obj.{v, v, u, u} (shiftFunctor C (0 + a)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd C 0 a)) X)
    (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫ eqToHom ⋯)

Tactic:
simp [← shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, 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
⊢ 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.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C a) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_add_zero C a)) X

Premises used: CategoryTheory.shiftFunctorAdd'_add_zero, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.hom
-- 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
dsimp : obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C a) X)

Tactic:
dsimp
-- 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
rw rw₁ : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (shiftFunctor C a) X

Tactic:
rw [add_zero]

Premises used: add_zero
-- 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} (shiftFunctor C (a + 0)) 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)) X)
    (eqToHom ⋯ ≫ NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C a) X))

Tactic:
simp [← shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.shiftFunctorAdd'_add_zero_hom_app