awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (A.map f ≫ NatTrans.app ε Y : A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
have rw : Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X) (NatTrans.app ε X)
      (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
    A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y)
  (NatTrans.app ε X :
    A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
Tactic: rw [ε[A].naturality, tensorUnit_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
        (NatTrans.app ε X :
          A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
        (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
      A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
have rw : Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
  (NatTrans.app ε X :
    A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
  (NatTrans.app ε X)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Comon.X (functorObjObj A X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (Comon.X (functorObjObj A Y)) (Comon.X (functorObjObj A Y)))
    (A.map f ≫ Δ) (Δ ≫ (A.map f ⊗ₘ A.map f))
have dsimp : Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
  (A.map f ≫ NatTrans.app Δ Y : A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
      (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f) :
    A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
⊢ Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (A.map f ≫ NatTrans.app Δ Y : A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
        (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f) :
      A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
have rw : Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
  (NatTrans.app Δ X ≫ (tensorObj (𝒞 := Functor.category) A A).map f)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
    (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f))
Tactic: rw [Δ[A].naturality, tensorObj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (NatTrans.app Δ X ≫ (tensorObj (𝒞 := Functor.category) A A).map f)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
      (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f))
⊢ Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (A.map f ≫ NatTrans.app Δ Y : A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
        (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f) :
      A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
have rw₁ : Eq.{v₂ + 1} (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
  (CategoryStruct.comp (Y := (tensorObj (𝒞 := Functor.category) A A).obj X) (NatTrans.app Δ X) (A.map f ⊗ₘ A.map f))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
    (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f))
Tactic: rw [Δ[A].naturality, tensorObj_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
⊢ Eq (α := Quiver.Hom (V := Comon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A X))
    { hom := A.map (𝟙 X), isComonHom_hom := ⋯ } (𝟙 (functorObjObj A X))
have w : Eq (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A X))
  (Comon.Hom.hom { hom := A.map (𝟙 X), isComonHom_hom := sorry }) (Comon.Hom.hom (𝟙 (functorObjObj A X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
⊢ Eq (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A X))
    (Comon.Hom.hom { hom := A.map (𝟙 X), isComonHom_hom := ⋯ }) (Comon.Hom.hom (𝟙 (functorObjObj A X)))
have w : A.map (𝟙 X) = 𝟙 (A.obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)
have w : Eq.{v₂ + 1} (α := A.obj X ⟶ A.obj X) (𝟙 (A.obj X)) (𝟙 (A.obj X))
Tactic: rw [CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := Quiver.Hom (V := Comon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A Z))
    { hom := A.map (f ≫ g), isComonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := ⋯ }
      { hom := A.map g, isComonHom_hom := ⋯ })
have w : Eq.{v₂ + 1} (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A Z))
  (Comon.Hom.hom { hom := A.map (f ≫ g), isComonHom_hom := sorry })
  (Comon.Hom.hom
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := sorry }
      { hom := A.map g, isComonHom_hom := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A Z))
    (Comon.Hom.hom { hom := A.map (f ≫ g), isComonHom_hom := ⋯ })
    (Comon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := ⋯ }
        { hom := A.map g, isComonHom_hom := ⋯ }))
have w : A.map (f ≫ g) = A.map f ≫ A.map g
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ A.map (f ≫ g) = A.map f ≫ A.map g
have w : A.map f ≫ A.map g = A.map f ≫ A.map g
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
⊢ Eq (α := (inverseObj X).X ⟶ (𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category))
    (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ε) ε
have w : ∀ (x : C),
  Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) x)
    (NatTrans.app
      (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := sorry } ε) x)
    (NatTrans.app ε x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
⊢ Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) x)
    (NatTrans.app
      (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ε) x)
    (NatTrans.app ε x)
have w : Eq (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ((α.app x).hom ≫ ε) ε
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
⊢ Eq (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ((α.app x).hom ≫ ε) ε
have w : Eq.{v₂ + 1} (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ε ε
Tactic: rw [IsComonHom.hom_counit (α.app x).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
⊢ Eq (α := (inverseObj X).X ⟶ tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X)
    ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ≫ Δ)
    (Δ ≫
      ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
        { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X }))
have w : ∀ (x : C),
  Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶ (tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X).obj x)
    (NatTrans.app ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := sorry } ≫ Δ) x)
    (NatTrans.app
      (Δ ≫
        ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := sorry : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
          { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := sorry : NatTrans (inverseObj X).X (inverseObj Y).X }))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
⊢ Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶ (tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X).obj x)
    (NatTrans.app ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ≫ Δ) x)
    (NatTrans.app
      (Δ ≫
        ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
          { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X }))
      x)
have w : Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X) ((α.app x).hom ≫ Δ)
  (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
⊢ Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X) ((α.app x).hom ≫ Δ)
    (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
have w : Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X) (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
  (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
Tactic: rw [IsComonHom.hom_comul (α.app x).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F : C ⥤ CommMon.{v₂, u₂} D
⊢ Eq (α :=
    tensorObj (𝒞 := Functor.category)
        (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
        (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X ⟶
      (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X)
    (Iso.hom
        (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
          (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
      μ)
    μ
have w : ∀ (X : C),
  Eq (α :=
    (tensorObj (𝒞 := Functor.category)
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X).obj
        X ⟶
      (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X.obj X)
    (NatTrans.app
      (Iso.hom
          (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
        μ)
      X)
    (NatTrans.app μ X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Limits (hypothesis)
Goal:
J : Type w
inst : Category.{v_1, w} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
F : J ⥤ Mon.{v, u} C
c : Cone (F ⋙ forget C)
hc : IsLimit c
i j : J
f : i ⟶ j
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v_1, v, w, u} (Functor.obj (Functor.const J) (tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1)) i ⟶
      (F ⋙ forget C).obj j)
    (Functor.map (Functor.obj (Functor.const J) (tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1)) f ≫
      (c.π.app j ⊗ₘ c.π.app j) ≫ μ)
    (((c.π.app i ⊗ₘ c.π.app i) ≫ μ) ≫ (F ⋙ forget C).map f)
have this : Functor.map (Functor.obj (Functor.const J) c.pt) f ≫ c.π.app j = c.π.app i ≫ (F ⋙ forget C).map f
Tactic: have := c.π.naturality f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Limits (goal)
Goal:
J : Type w
inst : Category.{v_1, w} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
F : J ⥤ Mon.{v, u} C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
h : J
⊢ { hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h = s.π.app h
have w : Hom.hom ({ hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := sorry } ≫ (limitCone F c hc).π.app h) =
  (s.π.app h).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ 1 * x = x
have h : x =
  (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
      (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
        (↑A : Type u))
    (1 ⊗ₜ[R] x)
Tactic: convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) ((1 : R) ⊗ₜ x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ x =
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
          (↑A : Type u))
      (1 ⊗ₜ[R] x)
have h : x = HSMul.hSMul (α := R) 1 x
Tactic: rw [MonoidalCategory.leftUnitor_hom_apply, one_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
h : x = HSMul.hSMul (α := R) 1 x
⊢ x =
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
        (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
          (↑A : Type u))
      (1 ⊗ₜ[R] x)
have h₁ : x = x
Tactic: rw [MonoidalCategory.leftUnitor_hom_apply, one_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ x * 1 = x
have h : x =
  (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
      (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
        (↑A : Type u))
    (x ⊗ₜ[R] 1)
Tactic: convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (x ⊗ₜ (1 : R))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ x =
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
        (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
          (↑A : Type u))
      (x ⊗ₜ[R] 1)
have h : x = HSMul.hSMul (α := R) 1 x
Tactic: rw [MonoidalCategory.rightUnitor_hom_apply, one_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
h : x = HSMul.hSMul (α := R) 1 x
⊢ x =
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
        (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
          (↑A : Type u))
      (x ⊗ₜ[R] 1)
have h₁ : x = x
Tactic: rw [MonoidalCategory.rightUnitor_hom_apply, one_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        (0 ⊗ₜ[R] x) :
      (↑A : Type u))
    (0 : (↑A : Type u))
have rw : Eq (α := (↑A : Type u))
  ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier
          _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
        (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
      0 :
    (↑A : Type u))
  (0 : (↑A : Type u))
Tactic: rw [TensorProduct.zero_tmul, map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
rw :
  Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        0 :
      (↑A : Type u))
    (0 : (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        (0 ⊗ₜ[R] x) :
      (↑A : Type u))
    (0 : (↑A : Type u))
have rw₁ : Eq.{u + 1} (α := (↑A : Type u)) 0 0
Tactic: rw [TensorProduct.zero_tmul, map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        (x ⊗ₜ[R] 0) :
      (↑A : Type u))
    (0 : (↑A : Type u))
have rw : Eq (α := (↑A : Type u))
  ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier
          _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
        (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
      0 :
    (↑A : Type u))
  (0 : (↑A : Type u))
Tactic: rw [TensorProduct.tmul_zero, map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
rw :
  Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        0 :
      (↑A : Type u))
    (0 : (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) _ μ :
          (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
        (x ⊗ₜ[R] 0) :
      (↑A : Type u))
    (0 : (↑A : Type u))
have rw₁ : Eq.{u + 1} (α := (↑A : Type u)) 0 0
Tactic: rw [TensorProduct.tmul_zero, map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ x * (y + z) = x * y + x * z
have h : x * (y + z) =
  (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
    (HAdd.hAdd (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) : Type u)) (x ⊗ₜ[R] y)
      (x ⊗ₜ[R] z))
Tactic: convert! μ[A].hom.map_add (x ⊗ₜ y) (x ⊗ₜ z)