awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
this : Functor.map (Functor.obj (Functor.const J) c.pt) f ≫ c.π.app j = c.π.app i ≫ (F ⋙ forget C).map f
⊢ 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)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) c.pt ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift { pt := tensorUnit.{v, u} C (𝒞 := inst_1), π := { app := fun (X : J) ↦ η, naturality := ⋯ } } ▷
                c.pt :
              tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) c.pt ⟶
                tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
              Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                c.pt) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) c.pt ⟶ (F ⋙ forget C).obj j)
      (Iso.hom (λ_ c.pt) ≫ c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) c.pt ⟶ (F ⋙ forget C).obj j)

Tactic:
simp [whiskerRight_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerRight_comp_tensorHom_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    Eq (α := tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (c.pt ◁
                hc.lift { pt := tensorUnit.{v, u} C (𝒞 := inst_1), π := { app := fun (X : J) ↦ η, naturality := ⋯ } } :
              tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶
                tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
              Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                c.pt) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ (F ⋙ forget C).obj j)
      (Iso.hom (ρ_ c.pt) ≫ c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ (F ⋙ forget C).obj j)

Tactic:
simp [whiskerLeft_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp_tensorHom_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷
                c.pt :
              tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶
                tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
              Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                c.pt) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)
      ((Iso.hom (α_ c.pt c.pt c.pt) ≫
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
              (c.pt ◁
                  hc.lift
                    { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                      π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
                tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) ⟶
                  tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
              (hc.lift
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
                Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                    { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                      π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                  c.pt)) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsLimit.fac,
      mon_tauto, implies_true]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Mon.forget_obj, implies_true, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    NatTrans.app (Cone.π (Functor.mapCone (forget C) (limitCone F c hc))) j =
      Iso.hom (Iso.refl (Cone.pt (F := F ⋙ forget C) (Functor.mapCone (forget C) (limitCone F c hc)))) ≫ c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    Eq (α := tensorUnit.{v, u} C (𝒞 := inst_1) ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := s.pt.X) (η : tensorUnit.{v, u} C (𝒞 := inst_1) ⟶ s.pt.X)
          (hc.lift (Functor.mapCone (forget C) s) : Cone.pt (F := F ⋙ forget C) (Functor.mapCone (forget C) s) ⟶ c.pt) ≫
        c.π.app j)
      (η ≫ c.π.app j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
⊢ ∀ (j : J),
    Eq (α := tensorObj.{v, u} (𝒞 := inst_1) s.pt.X s.pt.X ⟶ (F ⋙ forget C).obj j)
      ((μ ≫ hc.lift (Functor.mapCone (forget C) s)) ≫ c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) s.pt.X s.pt.X ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limitCone F c hc).pt.X (limitCone F c hc).pt.X)
            (hc.lift (Functor.mapCone (forget C) s) ⊗ₘ hc.lift (Functor.mapCone (forget C) s)) μ ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) s.pt.X s.pt.X ⟶ (F ⋙ forget C).obj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
w :
  Hom.hom ({ hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h) =
    (s.π.app h).hom
⊢ { hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h = s.π.app h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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.hom ({ hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := ⋯ } ≫ (limitCone F c hc).π.app h) =
    (s.π.app h).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
m : s.pt ⟶ (limitCone F c hc).pt
w : ∀ (j : J), m ≫ (limitCone F c hc).π.app j = s.π.app j
j : J
⊢ m.hom ≫ c.π.app j = Hom.hom { hom := hc.lift (Functor.mapCone (forget C) s), isMonHom_hom := ⋯ } ≫ c.π.app j

Tactic:
simpa using congr($(w j).hom)
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
inst_3 : HasLimitsOfShape.{v_1, w, v, u} J C
⊢ HasLimitsOfShape J (Mon.{v, u} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (forget C)

Premises used: CategoryTheory.Mon.forget, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
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
inst_3 : HasLimitsOfShape.{v_1, w, v, u} J C
⊢ PreservesLimitsOfShape (C := Mon.{v, u} C) J (forget C)

Tactic:
CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape _

Premises used: CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight μ A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj A A) A) : Type u)) → (↑A : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.associator A A A) ≫ MonoidalCategoryStruct.whiskerLeft A μ ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj A A) A) : Type u)) → (↑A : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑A : Type u))

Tactic:
LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_assoc A)) (x ⊗ₜ y ⊗ₜ z)

Premises used: CategoryTheory.MonObj.mul_assoc, ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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 * z)

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_assoc A)) (x ⊗ₜ y ⊗ₜ z)

Premises used: CategoryTheory.MonObj.mul_assoc, ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (1 ⊗ₜ[R] x) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (1 ⊗ₜ[R] x) :
      (↑A : Type u))

Tactic:
LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) ((1 : R) ⊗ₜ x)

Premises used: ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul, OfNat.ofNat, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
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)
⊢ 1 * x = x

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) ((1 : R) ⊗ₜ x)

Premises used: ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul, OfNat.ofNat, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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
h₁ h₂ : x = 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)

Tactic:
rw [MonoidalCategory.leftUnitor_hom_apply, one_smul]

Premises used: ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R] 1) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R] 1) :
      (↑A : Type u))

Tactic:
LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (x ⊗ₜ (1 : R))

Premises used: CategoryTheory.MonObj.mul_one, ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x : (↑A : Type u)
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)
⊢ x * 1 = x

Tactic:
convert! LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (x ⊗ₜ (1 : R))

Premises used: CategoryTheory.MonObj.mul_one, ModuleCat.hom_ext_iff, LinearMap.congr_fun, Iff.mp, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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
h₁ h₂ : x = 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)

Tactic:
rw [MonoidalCategory.rightUnitor_hom_apply, one_smul]

Premises used: ModuleCat.MonoidalCategory.rightUnitor_hom_apply, one_smul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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))
rw₁ rw₂ : Eq.{u + 1} (α := (↑A : Type u)) 0 0
⊢ 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))

Tactic:
rw [TensorProduct.zero_tmul, map_zero]

Premises used: map_zero, TensorProduct.zero_tmul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
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))
rw₁ rw₂ : Eq.{u + 1} (α := (↑A : Type u)) 0 0
⊢ 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))

Tactic:
rw [TensorProduct.tmul_zero, map_zero]

Premises used: TensorProduct.tmul_zero, map_zero
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ (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)) =
    HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
      ((Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (x ⊗ₜ[R] y) :
        (↑A : Type u))
      ((Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (x ⊗ₜ[R] z) :
        (↑A : Type u))

Tactic:
μ[A].hom.map_add (x ⊗ₜ y) (x ⊗ₜ z)

Premises used: LinearMap.map_add, TensorProduct.tmul, ModuleCat.Hom.hom, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
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))
⊢ x * (y + z) = x * y + x * z

Tactic:
convert! μ[A].hom.map_add (x ⊗ₜ y) (x ⊗ₜ z)

Premises used: LinearMap.map_add, TensorProduct.tmul, ModuleCat.Hom.hom, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
h :
  x * (y + z) = (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (x ⊗ₜ[R] (y + z))
⊢ 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:
rw [← TensorProduct.tmul_add]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ x * (y + z) = (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (x ⊗ₜ[R] (y + z))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u))
      (HAdd.hAdd (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A A) : Type u)) (x ⊗ₜ[R] z)
        (y ⊗ₜ[R] z)) =
    HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
      ((Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (x ⊗ₜ[R] z) :
        (↑A : Type u))
      ((Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) (y ⊗ₜ[R] z) :
        (↑A : Type u))

Tactic:
μ[A].hom.map_add (x ⊗ₜ z) (y ⊗ₜ z)

Premises used: LinearMap.map_add, TensorProduct.tmul, ModuleCat.Hom.hom, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
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] z)
        (y ⊗ₜ[R] z))
⊢ (x + y) * z = x * z + y * z

Tactic:
convert! μ[A].hom.map_add (x ⊗ₜ z) (y ⊗ₜ z)

Premises used: LinearMap.map_add, TensorProduct.tmul, ModuleCat.Hom.hom, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
h :
  (x + y) * z = (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) ((x + y) ⊗ₜ[R] z)
⊢ (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] z)
        (y ⊗ₜ[R] z))

Tactic:
rw [← TensorProduct.add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y z : (↑A : Type u)
⊢ (x + y) * z = (Hom.hom μ : (a : (↑(MonoidalCategoryStruct.tensorObj A A) : Type u)) → (↑A : Type u)) ((x + y) ⊗ₜ[R] z)

Tactic:
rfl