awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
V_1 : Type u₂
inst_1 : Category.{v₂, u₂} V_1
inst_2 : MonoidalCategory.{v₁, u₁} C_1
inst_3 : MonoidalCategory.{v₂, u₂} V_1
C : Type u₁
inst_4 : Category.{v₁, u₁} C
V : Type u₂
inst_5 : Category.{v₂, u₂} V
inst_6 : MonoidalCategory.{v₁, u₁} C
inst_7 : MonoidalCategory.{v₂, u₂} V
D : Type u₃
inst_8 : Category.{v₃, u₃} D
inst_9 : InducedLawfulDayConvolutionMonoidalCategoryStructCore.{v₁, v₂, v₃, u₁, u₂, u₃} C V D
d d' : D
X Y : C × C
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α :=
    Functor.obj.{v₁, v₂, u₁, u₂}
        (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') X ⟶
      Functor.obj.{v₁, v₂, u₁, u₂}
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        Y)
    (Functor.map (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') f ≫
      convolutionUnitApp V d d' Y.1 Y.2)
    (convolutionUnitApp V d d' X.1 X.2 ≫
      Functor.map
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        f)
have simp : Eq.{v₂ + 1} (α :=
  Functor.obj.{v₁, v₂, u₁, u₂}
      (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d ⊠ Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') X ⟶
    Functor.obj.{v₁, v₂, u₁, u₂}
      (tensor C ⋙
        Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
          (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
      Y)
  (CategoryStruct.comp (Y :=
    Functor.obj.{v₁, v₂, u₁, u₂}
      (tensor C ⋙
        @DayConvolution.convolution _ _ _ _ inst_6 inst_7 (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
          (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') _)
      X)
    (NatTrans.app
      (DayConvolution.unit (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
        (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d'))
      X)
    (Functor.map
        (tensor C ⋙
          @DayConvolution.convolution _ _ _ _ inst_6 inst_7 (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
            (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d') _)
        f ≫
      NatTrans.app (Iso.inv (tensorObjIsoConvolution C V d d'))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst_4) Y.1 Y.2)))
  (NatTrans.app
      (DayConvolution.unit (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d)
        (Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _) d'))
      (X.1, X.2) ≫
    NatTrans.app (Iso.inv (tensorObjIsoConvolution C V d d'))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst_4) X.1 X.2) ≫
      Functor.map
        (tensor C ⋙
          Functor.obj (@ι C _ V _ inst_6 inst_7 D _ _)
            (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst_4 V inst_5 inst_6 inst_7 _ inst_8 _ d d'))
        f)
Tactic: simp only [convolutionUnitApp_eq, Category.assoc, NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
D : Type u₃
inst_4 : Category.{v₃, u₃} D
inst_5 : InducedLawfulDayConvolutionMonoidalCategoryStructCore.{v₁, v₂, v₃, u₁, u₂, u₃} C V D
inst_6 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))) d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))) d)
      (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₂, u₁, u₂} C V)
      (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _) (MonoidalCategoryStruct.tensorObj.{v₃, u₃} (𝒞 := inst_4) d₁ d₁'))
      (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _) (MonoidalCategoryStruct.tensorObj.{v₃, u₃} (𝒞 := inst_4) d₂ d₂')))
    (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) (f ⊗ₘ f'))
    (DayConvolution.map (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f)
      (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f'))
have dsimp : Eq (α :=
  Quiver.Hom (V := Functor.{v₁, v₂, u₁, u₂} C V)
    (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
      (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₁ d₁'))
    (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
      (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₂ d₂')))
  (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) (tensorHom f f'))
  (DayConvolution.map (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f)
    (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f'))
Tactic: dsimp +instances [mkMonoidalCategoryStruct]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
D : Type u₃
inst_4 : Category.{v₃, u₃} D
inst_5 : InducedLawfulDayConvolutionMonoidalCategoryStructCore.{v₁, v₂, v₃, u₁, u₂, u₃} C V D
inst_6 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorLeft v)
inst_7 :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow.{v₁, v₁, u₁, u₁} (tensor C) d) (tensorRight v)
inst_8 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))) d)
      (tensorRight v)
inst_9 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))) d)
      (tensorLeft v)
d₁ d₁' d₂ d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₂, u₁, u₂} C V)
      (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
        (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₁ d₁'))
      (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
        (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₂ d₂')))
    (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) (tensorHom f f'))
    (DayConvolution.map (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f)
      (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f'))
have rw : Eq (α :=
  Quiver.Hom (V := Functor.{v₁, v₂, u₁, u₂} C V)
    (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
      (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₁ d₁'))
    (Functor.obj (@ι C _ V _ inst_2 inst_3 D _ _)
      (@tensorObj.{v₁, v₂, v₃, u₁, u₂, u₃} C inst V inst_1 inst_2 inst_3 _ inst_4 _ d₂ d₂')))
  (Iso.hom (tensorObjIsoConvolution C V d₁ d₁') ≫
    DayConvolution.map (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f)
        (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f') ≫
      Iso.inv (tensorObjIsoConvolution C V d₂ d₂'))
  (DayConvolution.map (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f)
    (Functor.map (@ι C _ V _ inst_2 inst_3 D _ _) f'))
Tactic: rw [tensorHom_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
X x x_1 : Discrete M
f : x ⟶ x_1
⊢ { as := X.as * x.as : Discrete M } = { as := X.as * x_1.as }
have rw : { as := X.as * x_1.as : Discrete M } = { as := X.as * x_1.as }
Tactic: rw [eq_of_hom f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
X₁ X₂ : Discrete M
f : X₁ ⟶ X₂
X : Discrete M
⊢ { as := X₁.as * X.as : Discrete M } = { as := X₂.as * X.as }
have rw : { as := X₂.as * X.as : Discrete M } = { as := X₂.as * X.as }
Tactic: rw [eq_of_hom f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
X₁ Y₁ X₂ Y₂ : Discrete M
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ { as := X₁.as * X₂.as : Discrete M } = { as := Y₁.as * Y₂.as }
have rw : { as := Y₁.as * X₂.as : Discrete M } = { as := Y₁.as * Y₂.as }
Tactic: rw [eq_of_hom f, eq_of_hom g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
X₁ Y₁ X₂ Y₂ : Discrete M
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
rw : { as := Y₁.as * X₂.as : Discrete M } = { as := Y₁.as * Y₂.as }
⊢ { as := X₁.as * X₂.as : Discrete M } = { as := Y₁.as * Y₂.as }
have rw₁ : { as := Y₁.as * Y₂.as : Discrete M } = { as := Y₁.as * Y₂.as }
Tactic: rw [eq_of_hom f, eq_of_hom g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
⊢ Eq (α :=
    (𝟙_ (Discrete K)) (𝒞 := discreteCategory K) ⟶
      (monoidalFunctor (G.comp F)).obj ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)))
    (ε (monoidalFunctor F ⋙ monoidalFunctor G) ≫
      (monoidalFunctorComp F G).hom.app ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)))
    (ε (monoidalFunctor (G.comp F)))
have dsimp : (Discrete.eqToHom sorry ≫ (monoidalFunctor G).map (Discrete.eqToHom sorry)) ≫
    NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)) =
  Discrete.eqToHom sorry
Tactic: dsimp only [comp_ε, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_ε]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Discrete (goal)
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
x x_1 : Discrete M
⊢ Eq (α :=
    tensorObj (𝒞 := discreteCategory K) ((monoidalFunctor F ⋙ monoidalFunctor G).obj x)
        ((monoidalFunctor F ⋙ monoidalFunctor G).obj x_1) ⟶
      (monoidalFunctor (G.comp F)).obj (tensorObj (𝒞 := discreteCategory M) x x_1))
    (μ (monoidalFunctor F ⋙ monoidalFunctor G) x x_1 ≫
      (monoidalFunctorComp F G).hom.app (tensorObj (𝒞 := discreteCategory M) x x_1))
    (((monoidalFunctorComp F G).hom.app x ⊗ₘ (monoidalFunctorComp F G).hom.app x_1) ≫
      μ (monoidalFunctor (G.comp F)) x x_1)
have dsimp : Eq (α :=
  tensorObj (𝒞 := discreteCategory K) ((monoidalFunctor F ⋙ monoidalFunctor G).obj x)
      ((monoidalFunctor F ⋙ monoidalFunctor G).obj x_1) ⟶
    (monoidalFunctor (G.comp F)).obj (tensorObj (𝒞 := discreteCategory M) x x_1))
  ((Discrete.eqToHom sorry ≫ (monoidalFunctor G).map (Discrete.eqToHom sorry)) ≫
    NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) (tensorObj (𝒞 := discreteCategory M) x x_1))
  ((NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x ⊗ₘ
      NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x_1) ≫
    Discrete.eqToHom sorry)
Tactic: dsimp only [comp_μ, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ NatTrans.app (μ F m' n') X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (f ⊗ₘ g)) X)
have this : Eq (α :=
  (tensorObj (𝒞 := Functor.category) (F.obj m) (F.obj n)).obj X ⟶
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n')).obj X)
  (NatTrans.app ((F.map f ⊗ₘ F.map g) ≫ μ F m' n') X) (NatTrans.app (μ F m n ≫ F.map (f ⊗ₘ g)) X)
Tactic: have := congr_app (μ_natural F f g) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n m' : M
f : m ⟶ m'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n)).obj X)
    ((F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (f ▷ n)) X)
have rw : Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n)).obj X)
  ((F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
  ((F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
Tactic: rw [← tensorHom_id, ← μ_naturality₂ F f (𝟙 n) X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m n n' : M
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ NatTrans.app (μ F m n') X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (m ◁ g)) X)
have rw : Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n')).obj X)
  ((F.map g).app ((F.obj m).obj X) ≫ NatTrans.app (μ F m n') X)
  ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ NatTrans.app (μ F m n') X)
Tactic: rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X) ⟶
      (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
    ((F.obj n).map (NatTrans.app (ε F) X))
    (NatTrans.app (F.map (Iso.inv (λ_ n))) X ≫ NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
have rw : Eq (α :=
  (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X) ⟶
    (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
  ((F.obj n).map (NatTrans.app (ε F) X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
    (NatTrans.app (Iso.inv (λ_ (F.obj n)) ≫ ε F ▷ F.obj n ≫ μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
    (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X))
Tactic: rw [map_leftUnitor_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X) ⟶
      (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
    ((F.obj n).map (NatTrans.app (ε F) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
      (NatTrans.app (Iso.inv (λ_ (F.obj n)) ≫ ε F ▷ F.obj n ≫ μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
      (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X))
have dsimp : Eq (α := (F.obj n).obj X ⟶ (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
  ((F.obj n).map (NatTrans.app (ε F) X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
    (𝟙 ((F.obj n).obj X) ≫
      (F.obj n).map (NatTrans.app (ε F) X) ≫ NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
    (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) ⟶
      (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X))
    ((F.obj n).map (NatTrans.app (η F) X))
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X ≫ NatTrans.app (F.map (Iso.hom (λ_ n))) X)
have rw : Eq (α :=
  (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) ⟶
    (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
  ((F.obj n).map (NatTrans.app (η F) X ≫ NatTrans.app (ε F) X))
  ((NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X ≫ NatTrans.app (F.map (Iso.hom (λ_ n))) X) ≫
    (F.obj n).map (NatTrans.app (ε F) X))
Tactic: rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (NatTrans.app (F.map (Iso.inv (ρ_ n))) X ≫ NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
have rw : Eq (α :=
  Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
  (NatTrans.app (ε F) ((F.obj n).obj X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
    (NatTrans.app (Iso.inv (ρ_ (F.obj n)) ≫ F.obj n ◁ ε F ≫ μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
    (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))
Tactic: rw [map_rightUnitor_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (Iso.inv (ρ_ (F.obj n)) ≫ F.obj n ◁ ε F ≫ μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))
have dsimp : Eq (α := (F.obj n).obj X ⟶ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
  (NatTrans.app (ε F) ((F.obj n).obj X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
    (𝟙 ((F.obj n).obj X) ≫
      NatTrans.app (ε F) ((F.obj n).obj X) ≫ NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
    (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
    (NatTrans.app (η F) ((F.obj n).obj X))
    (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫ NatTrans.app (F.map (Iso.hom (ρ_ n))) X)
have rw : Eq (α :=
  (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
  (NatTrans.app (η F) ((F.obj n).obj X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
    (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
    (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) ≫ F.obj n ◁ η F ≫ Iso.hom (ρ_ (F.obj n))) X))
Tactic: rw [map_rightUnitor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (goal)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
    (NatTrans.app (η F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) ≫ F.obj n ◁ η F ≫ Iso.hom (ρ_ (F.obj n))) X))
have dsimp : Eq (α := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
  (NatTrans.app (η F) ((F.obj n).obj X))
  (CategoryStruct.comp (Y :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
    (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
    (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫
      NatTrans.app (η F) ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.End (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
      NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X)
    (NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫ NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)
have this : Eq (α :=
  (tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)) (F.obj m₃)).obj X ⟶
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
  (NatTrans.app
    (μ F m₁ m₂ ▷ F.obj m₃ ≫ μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫ F.map (Iso.hom (α_ m₁ m₂ m₃))) X)
  (NatTrans.app
    (Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
      F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
    X)
Tactic: have := congr_app (associativity F m₁ m₂ m₃) X