awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
W : SemimoduleCat.{u_1, u} R
X : SemimoduleCat.{u_2, u} R
Y : SemimoduleCat.{u_3, u} R
Z : SemimoduleCat.{u_4, u} R
hf :
  ∀ (w : (↑W : Type u_1)) (x : (↑X : Type u_2)) (y : (↑Y : Type u_3)) (z : (↑Z : Type u_4)),
    Eq (α := (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
      ((Hom.hom
              (whiskerRight (associator W X Y).hom Z ≫
                Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) :
            (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
              (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
          (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
      ((Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z))) :
            (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
              (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
          (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
⊢ Hom.hom
      (whiskerRight (associator W X Y).hom Z ≫
        Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) =
    Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z)))

Tactic:
apply TensorProduct.ext_fourfold

Premises used: TensorProduct.ext_fourfold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
W : SemimoduleCat.{u_1, u} R
X : SemimoduleCat.{u_2, u} R
Y : SemimoduleCat.{u_3, u} R
Z : SemimoduleCat.{u_4, u} R
w : (↑W : Type u_1)
x : (↑X : Type u_2)
y : (↑Y : Type u_3)
z : (↑Z : Type u_4)
⊢ Eq (α := (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
    ((Hom.hom
            (whiskerRight (associator W X Y).hom Z ≫
              Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) :
          (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
            (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
    ((Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z))) :
          (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
            (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf : Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf :
  LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
      (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f))
⊢ Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)

Tactic:
apply TensorProduct.ext

Premises used: TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf :
  ∀ (x : (↑M : Type u)),
    Eq (α := (↑N : Type u))
      ((((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
                    (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) :
                  (↑(of R R) : Type u) →ₗ[R] (↑M : Type u) →ₗ[R] (↑N : Type u)) :
                (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
              1 :
            (a : (↑M : Type u)) → (↑N : Type u))
          x :
        (↑N : Type u))
      (((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f)) :
                (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
              1 :
            (a : (↑M : Type u)) → (↑N : Type u))
          x :
        (↑N : Type u))
⊢ LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
      (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
x : (↑M : Type u)
⊢ Eq (α := (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
                  (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) :
                (↑(of R R) : Type u) →ₗ[R] (↑M : Type u) →ₗ[R] (↑N : Type u)) :
              (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
            1 :
          (a : (↑M : Type u)) → (↑N : Type u))
        x :
      (↑N : Type u))
    (((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f)) :
              (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
            1 :
          (a : (↑M : Type u)) → (↑N : Type u))
        x :
      (↑N : Type u))

Tactic:
simp [tensorHom, tensorObj, leftUnitor]

Premises used: SemimoduleCat.MonoidalCategory.tensorObj, SemimoduleCat.MonoidalCategory.leftUnitor, SemimoduleCat.MonoidalCategory.tensorHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf : Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf :
  LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
      (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f))
⊢ Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)

Tactic:
apply TensorProduct.ext

Premises used: TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
hf :
  ∀ (x : (↑M : Type u)),
    Eq (α := (↑N : Type u))
      ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
                    (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) :
                  (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
                x :
              (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
            (a : R) → (↑N : Type u))
          1 :
        (↑N : Type u))
      ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f)) :
                  (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
                x :
              (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
            (a : R) → (↑N : Type u))
          1 :
        (↑N : Type u))
⊢ LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
      (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
x : (↑M : Type u)
⊢ Eq (α := (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
                  (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) :
                (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
              x :
            (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
          (a : R) → (↑N : Type u))
        1 :
      (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f)) :
                (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
              x :
            (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
          (a : R) → (↑N : Type u))
        1 :
      (↑N : Type u))

Tactic:
simp [tensorHom, tensorObj, rightUnitor]

Premises used: SemimoduleCat.MonoidalCategory.tensorObj, SemimoduleCat.MonoidalCategory.tensorHom, SemimoduleCat.MonoidalCategory.rightUnitor
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
hf :
  Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))
⊢ Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
hf :
  ∀ (x : (↑M : Type u)) (y : (↑(of R R) : Type u)) (z : (↑N : Type u)),
    Eq (α := (↑(tensorObj M N) : Type u))
      ((Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))
      ((Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N)) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))
⊢ Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))

Tactic:
apply TensorProduct.ext_threefold

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
x : (↑M : Type u)
y : (↑(of R R) : Type u)
⊢ ∀ (z : (↑N : Type u)),
    Eq (α := (↑(tensorObj M N) : Type u))
      ((Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))
      ((Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N)) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))

Tactic:
TensorProduct.tmul_smul _ _

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul_smul, List.foldl, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
x : (↑M : Type u)
y : (↑(of R R) : Type u)
⊢ ∀ (z : (↑N : Type u)),
    Eq (α := (↑(tensorObj M N) : Type u))
      ((Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))
      ((Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N)) :
            (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(tensorObj M N) : Type u))

Tactic:
exact TensorProduct.tmul_smul _ _

Premises used: TensorProduct.tmul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
K L M N : SemimoduleCat R
f : K ⟶ L
g : M ⟶ N
⊢ Hom.hom (f ⊗ₘ g) = TensorProduct.map (Hom.hom f) (Hom.hom g)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
L M N : SemimoduleCat R
f : M ⟶ N
⊢ Hom.hom (L ◁ f) = LinearMap.lTensor (↑L : Type u) (Hom.hom f)

Tactic:
rfl

Premises used: LinearMap.lTensor, TensorProduct.map, TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
L M : SemimoduleCat R
f : L ⟶ M
N : SemimoduleCat R
⊢ Hom.hom (f ▷ N) = LinearMap.rTensor (↑N : Type u) (Hom.hom f)

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl, LinearMap.rTensor
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
⊢ Hom.hom (Iso.hom (λ_ M)) =
    (↑(TensorProduct.lid R (↑M : Type u)) : TensorProduct R R (↑M : Type u) →ₗ[R] (↑M : Type u))

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
⊢ Hom.hom (Iso.inv (λ_ M)) =
    (↑(LinearEquiv.symm (TensorProduct.lid R (↑M : Type u))) : (↑M : Type u) →ₗ[R] TensorProduct R R (↑M : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
⊢ Hom.hom (Iso.hom (ρ_ M)) =
    (↑(TensorProduct.rid R (↑M : Type u)) : TensorProduct R (↑M : Type u) R →ₗ[R] (↑M : Type u))

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
⊢ Hom.hom (Iso.inv (ρ_ M)) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (↑M : Type u))) : (↑M : Type u) →ₗ[R] TensorProduct R (↑M : Type u) R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N K : SemimoduleCat R
⊢ Hom.hom (Iso.hom (α_ M N K)) =
    (↑(TensorProduct.assoc R (↑M : Type u) (↑N : Type u) (↑K : Type u)) :
      TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u) →ₗ[R]
        TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)))

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N K : SemimoduleCat R
⊢ Hom.hom (Iso.inv (α_ M N K)) =
    (↑(LinearEquiv.symm (TensorProduct.assoc R (↑M : Type u) (↑N : Type u) (↑K : Type u))) :
      TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)) →ₗ[R]
        TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
K L M N : SemimoduleCat R
f : K ⟶ L
g : M ⟶ N
k : (↑K : Type u)
m : (↑M : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X := MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) K M) (f ⊗ₘ g) :
          (a : (↑(K ⊗ M) : Type u)) → (↑(L ⊗ N) : Type u))
        (k ⊗ₜ[R] m) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑K : Type u)) → (↑L : Type u))
          k ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              carrier) g :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
      TensorProduct R (↑L : Type u) (↑N : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
L M N : SemimoduleCat R
f : M ⟶ N
l : (↑L : Type u)
m : (↑M : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X := MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L M) (L ◁ f) :
          (a : (↑(L ⊗ M) : Type u)) → (↑(L ⊗ N) : Type u))
        (l ⊗ₜ[R] m) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    (l ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              carrier) f :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
      TensorProduct R (↑L : Type u) (↑N : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
L M : SemimoduleCat R
f : L ⟶ M
N : SemimoduleCat R
l : (↑L : Type u)
n : (↑N : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X := MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) L N) (f ▷ N) :
          (a : (↑(L ⊗ N) : Type u)) → (↑(M ⊗ N) : Type u))
        (l ⊗ₜ[R] n) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑L : Type u)) → (↑M : Type u))
          l ⊗ₜ[R]
        n :
      TensorProduct R (↑M : Type u) (↑N : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
r : R
m : (↑M : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (X :=
          MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) M)
          (Iso.hom (λ_ M)) :
        (a : (↑(𝟙_ (SemimoduleCat R) ⊗ M) : Type u)) → (↑M : Type u))
      (r ⊗ₜ[R] m) =
    r • m

Tactic:
TensorProduct.lid_tmul m r

Premises used: TensorProduct.lid_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
m : (↑M : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) M) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Y :=
            MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) M)
            (Iso.inv (λ_ M)) :
          (a : (↑M : Type u)) → (↑(𝟙_ (SemimoduleCat R) ⊗ M) : Type u))
        m :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) M) :
        Type u))
    (1 ⊗ₜ[R] m : TensorProduct R (↑((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) : Type u) (↑M : Type u))

Tactic:
TensorProduct.lid_symm_apply m

Premises used: TensorProduct.lid_symm_apply, Quotient, TensorProduct, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
m : (↑M : Type u)
r : R
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (X :=
          MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)))
          (Iso.hom (ρ_ M)) :
        (a : (↑(M ⊗ 𝟙_ (SemimoduleCat R)) : Type u)) → (↑M : Type u))
      (m ⊗ₜ[R] r) =
    r • m

Tactic:
TensorProduct.rid_tmul m r

Premises used: TensorProduct.rid_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat R
m : (↑M : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Y :=
            MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)))
            (Iso.inv (ρ_ M)) :
          (a : (↑M : Type u)) → (↑(M ⊗ 𝟙_ (SemimoduleCat R)) : Type u))
        m :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R))) :
        Type u))
    (m ⊗ₜ[R] 1 : TensorProduct R (↑M : Type u) (↑((𝟙_ (SemimoduleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
TensorProduct.rid_symm_apply m

Premises used: Quotient, TensorProduct.rid_symm_apply, TensorProduct, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N K : SemimoduleCat R
m : (↑M : Type u)
n : (↑N : Type u)
k : (↑K : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N K)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X :=
            MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) K)
            (Iso.hom (α_ M N K)) :
          (a : (↑((M ⊗ N) ⊗ K) : Type u)) → (↑(M ⊗ N ⊗ K) : Type u))
        (m ⊗ₜ[R] n ⊗ₜ[R] k) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N K)) :
        Type u))
    (m ⊗ₜ[R] (n ⊗ₜ[R] k) : TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M N K : SemimoduleCat R
m : (↑M : Type u)
n : (↑N : Type u)
k : (↑K : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) K) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X :=
            MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N K))
            (Iso.inv (α_ M N K)) :
          (a : (↑(M ⊗ N ⊗ K) : Type u)) → (↑((M ⊗ N) ⊗ K) : Type u))
        (m ⊗ₜ[R] (n ⊗ₜ[R] k)) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) K) :
        Type u))
    (m ⊗ₜ[R] n ⊗ₜ[R] k : TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl