awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₄ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₅ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom sorry)
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₄ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
rw₅ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom ⋯)
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₆ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (𝟙 ((h.F (n + 0)).obj X))
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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' }))
have 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 := sorry : 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 := sorry } } { as := X' }))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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 := ⋯ } }))
have 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 := sorry : 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 := sorry } }))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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 }))
have 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
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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 }))
have 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
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C k) (shiftFunctor C (i + j))
have rw : Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C k) (shiftFunctor C k)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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 (α := 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)
have 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) sorry)) (Iso.hom (shiftFunctorAdd C i j))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ Eq (α := Functor.{v, v, u, u} C C) (shiftFunctor C a) (shiftFunctor.{v, u, u_1} C (A := A) 0)
have 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)
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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))
have 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 sorry)) X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorZero C A)) (shiftFunctor C a)))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorZero C A)) (shiftFunctor C a)))
      X)
have 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 sorry) 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: dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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 (α :=
    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))
have 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 sorry ≫ 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 sorry)
    (NatTrans.app
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A)
        (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)) { as := a })
      X))
Tactic: simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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)))
have 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 sorry)) x)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (rightUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerLeft (shiftFunctor C a) (Iso.symm (shiftFunctorZero C A))))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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.hom
        (Iso.symm (rightUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerLeft (shiftFunctor C a) (Iso.symm (shiftFunctorZero C A))))
      x)
have 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 sorry) 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: dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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 (α :=
    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))
have 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 sorry ≫ 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 sorry)
    (NatTrans.app
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a }
        (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
      x))
Tactic: simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃
have rw₁ : a₁₂₃ = a₁₂₃
Tactic: rw [← h₁₂, h₁₂₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃
have rw : a₁ + (a₂ + a₃) = a₁₂₃
Tactic: rw [← h₂₃, ← add_assoc, h₁₂₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃
have rw₂ : a₁₂₃ = a₁₂₃
Tactic: rw [← h₂₃, ← add_assoc, h₁₂₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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₁₂₃
⊢ 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₂₃))
have 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₃) sorry ≪≫
    isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) sorry) (shiftFunctor C a₃) ≪≫
      associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
  (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) sorry ≪≫
    isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) sorry))
Tactic: subst h₁₂ h₂₃ h₁₂₃
Cleared hypotheses: a₁₂, a₂₃, a₁₂₃, h₁₂, h₂₃, h₁₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
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
⊢ 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₃) ⋯))
have 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₃) sorry ≪≫
          isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) sorry) (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₃) sorry ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) sorry)))
      X)
Tactic: ext X