awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f : (↑M₁ : Type u) → (↑M₂ : Type u) → (↑M₃ : Type u)
h₁ : ∀ (m₁ m₂ : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f (m₁ + m₂) n = f m₁ n + f m₂ n
h₂ : ∀ (a : R) (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f (a • m) n = a • f m n
h₃ : ∀ (m : (↑M₁ : Type u)) (n₁ n₂ : (↑M₂ : Type u)), f m (n₁ + n₂) = f m n₁ + f m n₂
h₄ : ∀ (a : R) (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f m (a • n) = a • f m n
m : (↑M₁ : Type u)
n : (↑M₂ : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (tensorLift f h₁ h₂ h₃ h₄) :
        (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u))
      (m ⊗ₜ[R] n) =
    f m n

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁ M₂ ⟶ M₃
h :
  ∀ (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u)) ((Hom.hom f : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
      ((Hom.hom g : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
h₁ :
  ∀ (x : (↑M₁ : Type u)) (x_1 : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u))
      ((((LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) :
                  (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
                x :
              (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
            (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
          x_1 :
        (↑M₃ : Type u))
      ((((LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g) :
                  (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
                x :
              (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
            (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
          x_1 :
        (↑M₃ : Type u))
⊢ LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) =
    LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁ M₂ ⟶ M₃
h :
  ∀ (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u)) ((Hom.hom f : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
      ((Hom.hom g : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
x : (↑M₁ : Type u)
x_1 : (↑M₂ : Type u)
⊢ Eq (α := (↑M₃ : Type u))
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) :
                (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
              x :
            (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
          (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
        x_1 :
      (↑M₃ : Type u))
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g) :
                (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
              x :
            (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
          (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
        x_1 :
      (↑M₃ : Type u))

Tactic:
apply h
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁ M₂) M₃ ⟶
    M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑((M₁ ⊗ M₂) ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              g :
            (a : (↑((M₁ ⊗ M₂) ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) :
        (↑M₄ : Type u))
⊢ f = g

Tactic:
hom_ext <| TensorProduct.ext_threefold h

Premises used: SemimoduleCat.hom_ext, TensorProduct.ext_threefold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶
    M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
rw : Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (α_ _ _ _).hom]

Premises used: CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶
    M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
⊢ Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g

Tactic:
tensor_ext₃' h

Premises used: SemimoduleCat.MonoidalCategory.tensor_ext₃'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶
    M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
⊢ Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g

Tactic:
exact tensor_ext₃' h

Premises used: SemimoduleCat.MonoidalCategory.tensor_ext₃'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.associator x x_1 x_2))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
          MonoidalCategoryStruct.associator (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x_1 x_2)))).hom

Tactic:
TensorProduct.ext (TensorProduct.ext rfl)

Premises used: Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.associator x x_1 x_2))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
          MonoidalCategoryStruct.associator (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
              (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_1)
                    (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x_2))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x_1 x_2)))).hom

Tactic:
exact TensorProduct.ext (TensorProduct.ext rfl)

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
hf :
  SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.leftUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
⊢ CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.leftUnitor x)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategory.tensorIso
            (Iso.symm
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
            (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
        MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.leftUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
TensorProduct.ext rfl

Premises used: Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.leftUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
            MonoidalCategory.tensorIso
              (Iso.symm
                (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
              (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
exact TensorProduct.ext rfl

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
hf :
  SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.rightUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
          MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
⊢ CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.rightUnitor x)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
            (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
        MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.rightUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
          MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
TensorProduct.ext rfl

Premises used: Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
⊢ SemimoduleCat.Hom.hom
      (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
        (Iso.hom (MonoidalCategoryStruct.rightUnitor x))) =
    SemimoduleCat.Hom.hom
      ((Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                  (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                    (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
              (Iso.symm
                (Iso.refl
                  (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
          MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom

Tactic:
exact TensorProduct.ext rfl

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
K L M N : ModuleCat R
f : K ⟶ L
g : M ⟶ N
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) K M) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    (Hom.hom (f ⊗ₘ g))
    (TensorProduct.map.{u, u, u, u, u, u} (R := R) (R₂ := R) (σ₁₂ := RingHom.id R) (M := (↑K : Type u)) (N :=
      (↑M : Type u)) (M₂ := (↑L : Type u)) (N₂ := (↑N : Type u)) (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 : CommRing R
L M N : ModuleCat R
f : M ⟶ N
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) L M) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    (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 : CommRing R
L M : ModuleCat R
f : L ⟶ M
N : ModuleCat R
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    (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 : CommRing R
M : ModuleCat 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 : CommRing R
M : ModuleCat 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 : CommRing R
M : ModuleCat 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 : CommRing R
M : ModuleCat 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 : CommRing R
M N K : ModuleCat 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