awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
r : R
Y Z : ModuleCat R
f : Y ⟶ Z
X : ModuleCat R
x : (↑Y : Type u)
y : (↑X : Type u)
refine_2 :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (r • f) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x ⊗ₜ[R]
      y =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            x ⊗ₜ[R]
          y :
        TensorProduct R (↑Z : Type u) (↑X : Type u))
⊢ (Hom.hom ((r • f) ▷ X) : (a : TensorProduct R (↑Y : Type u) (↑X : Type u)) → (↑(Z ⊗ X) : Type u)) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) r
      ((Hom.hom (f ▷ X) : (a : TensorProduct R (↑Y : Type u) (↑X : Type u)) → (↑(Z ⊗ X) : Type u)) (x ⊗ₜ[R] y) :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))

Tactic:
erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]

Premises used: ModuleCat.MonoidalCategory.whiskerRight_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
r : R
Y Z : ModuleCat R
f : Y ⟶ Z
X : ModuleCat R
x : (↑Y : Type u)
y : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (r • f) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x ⊗ₜ[R]
      y =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑Y : Type u)) → (↑Z : Type u))
            x ⊗ₜ[R]
          y :
        TensorProduct R (↑Z : Type u) (↑X : Type u))

Tactic:
simp [TensorProduct.smul_tmul, TensorProduct.tmul_smul]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M N P Q : ModuleCat R
f : (↑M : Type u) →ₗ[R] (↑N : Type u) →ₗ[R] (↑P : Type u)
g : (↑P : Type u) →ₗ[R] (↑Q : Type u)
⊢ ofHom₂ (f.compr₂ g) = ofHom₂ f ≫ ↟(Linear.rightComp R N (↟g))

Tactic:
rfl

Premises used: ModuleCat.ofHom₂, CategoryTheory.Linear.rightComp, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P
hf :
  Hom.hom
      ((fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
          Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
        ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
            (ofHom₂
                (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u)) (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
              N ⟶ of R (unop (op M) ⟶ P)))
          f)) =
    Hom.hom f
⊢ (fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
        Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
      ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
          (ofHom₂ (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u)) (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
            N ⟶ of R (unop (op M) ⟶ P)))
        f) =
    f

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P
hf :
  ∀ (x : (↑M : Type u)) (y : (↑N : Type u)),
    Eq (α := (↑P : Type u))
      (((Hom.hom
                ((fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
                    Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
                  ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
                      (ofHom₂
                          (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u))
                            (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
                        N ⟶ of R (unop (op M) ⟶ P)))
                    f)) :
              (↑(Functor.obj (MonoidalCategory.tensorLeft M) N) : Type u) →ₗ[R] (↑P : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u))
          (x ⊗ₜ[R] y) :
        (↑P : Type u))
      ((Hom.hom f : (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u)) (x ⊗ₜ[R] y) : (↑P : Type u))
⊢ Hom.hom
      ((fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
          Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
        ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
            (ofHom₂
                (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u)) (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
              N ⟶ of R (unop (op M) ⟶ P)))
          f)) =
    Hom.hom f

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P
⊢ ∀ (x : (↑M : Type u)) (y : (↑N : Type u)),
    Eq (α := (↑P : Type u))
      (((Hom.hom
                ((fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
                    Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
                  ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
                      (ofHom₂
                          (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u))
                            (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
                        N ⟶ of R (unop (op M) ⟶ P)))
                    f)) :
              (↑(Functor.obj (MonoidalCategory.tensorLeft M) N) : Type u) →ₗ[R] (↑P : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u))
          (x ⊗ₜ[R] y) :
        (↑P : Type u))
      ((Hom.hom f : (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u)) (x ⊗ₜ[R] y) : (↑P : Type u))

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M X' X Y : ModuleCat R
f : X' ⟶ X
g : X ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) Y
hf :
  Eq (α := (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u))
    (Hom.hom
      (((M.monoidalClosedHomEquiv X' Y).symm :
          (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
        ((M.monoidalClosedHomEquiv X Y).symm :
            (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
          g))
⊢ Eq (α := Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)
    (((M.monoidalClosedHomEquiv X' Y).symm :
          (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
        (f ≫ g) :
      Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)
    (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
        ((M.monoidalClosedHomEquiv X Y).symm :
            (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
          g :
      Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M X' X Y : ModuleCat R
f : X' ⟶ X
g : X ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) Y
hf :
  ∀ (x : (↑M : Type u)) (y : (↑X' : Type u)),
    Eq (α := (↑Y : Type u))
      (((Hom.hom
                (((M.monoidalClosedHomEquiv X' Y).symm :
                    (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                      (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
                  (f ≫ g)) :
              (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
          (x ⊗ₜ[R] y) :
        (↑Y : Type u))
      (((Hom.hom
                (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
                  ((M.monoidalClosedHomEquiv X Y).symm :
                      (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                        (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
                    g) :
              (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
          (x ⊗ₜ[R] y) :
        (↑Y : Type u))
⊢ Eq (α := (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u))
    (Hom.hom
      (((M.monoidalClosedHomEquiv X' Y).symm :
          (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
        ((M.monoidalClosedHomEquiv X Y).symm :
            (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
          g))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M X' X Y : ModuleCat R
f : X' ⟶ X
g : X ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) Y
m : (↑M : Type u)
n : (↑X' : Type u)
⊢ Eq (α := (↑Y : Type u))
    (((Hom.hom
              (((M.monoidalClosedHomEquiv X' Y).symm :
                  (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                    (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
                (f ≫ g)) :
            (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
        (m ⊗ₜ[R] n) :
      (↑Y : Type u))
    (((Hom.hom
              (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
                ((M.monoidalClosedHomEquiv X Y).symm :
                    (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                      (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
                  g) :
            (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
        (m ⊗ₜ[R] n) :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : N ⟶ P
g : (↑(of R (M ⟶ N)) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
          Functor.obj (ihom M) N) (CategoryTheory.Functor.map (ihom M) f) :
        (a : (↑((ihom M).obj N) : Type u)) → (↑((ihom M).obj P) : Type u))
      g =
    g ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : tensorObj (𝒞 := moduleCategory R) M N ⟶ P
x : (↑M : Type u)
y : (↑N : Type u)
⊢ Eq (α := (↑P : Type u))
    ((Hom.hom ((Hom.hom (MonoidalClosed.curry f) : (a : (↑N : Type u)) → (↑((ihom M).obj P) : Type u)) y) :
          (a : (↑(unop (op M)) : Type u)) → (↑P : Type u))
        x :
      (↑P : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑(M ⊗ N) : Type u)) → (↑P : Type u))
        (x ⊗ₜ[R] y) :
      (↑P : 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.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : N ⟶ Functor.obj (ihom M) P
x : (↑M : Type u)
y : (↑N : Type u)
⊢ Eq (α := (↑P : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (MonoidalClosed.uncurry f) :
          (a : (↑(M ⊗ N) : Type u)) → (↑P : Type u))
        (x ⊗ₜ[R] y) :
      (↑P : Type u))
    ((Hom.hom
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  carrier) f :
                (a : (↑N : Type u)) → (↑((ihom M).obj P) : Type u))
              y) :
          (a : (↑(unop (op M)) : Type u)) → (↑P : Type u))
        x :
      (↑P : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
rw :
  MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id))
⊢ Eq (α := Functor.obj (ihom M ⋙ tensorLeft M) N ⟶ Functor.obj (𝟭 (ModuleCat R)) N) (NatTrans.app (ihom.ev M) N)
    (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id)))

Tactic:
rw [← MonoidalClosed.uncurry_id_eq_ev]

Premises used: CategoryTheory.MonoidalClosed.uncurry_id_eq_ev
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
hf :
  Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) =
    Hom.hom
      (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
            (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
              TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
          (LinearMap.lcomp R (↑N : Type u)
              (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
            LinearMap.flip LinearMap.id)))
⊢ MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
hf :
  ∀ (x : (↑M : Type u)) (y : (↑(Functor.obj (ihom M) N) : Type u)),
    Eq (α := (↑N : Type u))
      ((Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) :
            (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
          (x ⊗ₜ[R] y) :
        (↑N : Type u))
      (((Hom.hom
                (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u)
                        (↑N : Type u) :
                      (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
                        TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
                    (LinearMap.lcomp R (↑N : Type u)
                        (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
                      LinearMap.flip LinearMap.id))) :
              (↑(tensorObj (𝒞 := moduleCategory R) M (Functor.obj (ihom M) N)) : Type u) →ₗ[R] (↑N : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
          (x ⊗ₜ[R] y) :
        (↑N : Type u))
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) =
    Hom.hom
      (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
            (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
              TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
          (LinearMap.lcomp R (↑N : Type u)
              (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
            LinearMap.flip LinearMap.id)))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
⊢ ∀ (x : (↑M : Type u)) (y : (↑(Functor.obj (ihom M) N) : Type u)),
    Eq (α := (↑N : Type u))
      ((Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) :
            (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
          (x ⊗ₜ[R] y) :
        (↑N : Type u))
      (((Hom.hom
                (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u)
                        (↑N : Type u) :
                      (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
                        TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
                    (LinearMap.lcomp R (↑N : Type u)
                        (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
                      LinearMap.flip LinearMap.id))) :
              (↑(tensorObj (𝒞 := moduleCategory R) M (Functor.obj (ihom M) N)) : Type u) →ₗ[R] (↑N : Type u)) :
            (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
          (x ⊗ₜ[R] y) :
        (↑N : Type u))

Tactic:
apply monoidalClosed_uncurry

Premises used: ModuleCat.monoidalClosed_uncurry
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
⊢ NatTrans.app (ihom.coev M) N =
    ofHom₂ (LinearMap.flip (TensorProduct.mk R (↑(unop (op M)) : Type u) (↑(Functor.obj (𝟭 (ModuleCat R)) N) : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.mk₂'ₛₗ, ModuleCat.ofHom₂, List.foldl, Quotient, LinearMap.flip, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : N ⟶ M
⊢ NatTrans.app (MonoidalClosed.pre f) P =
    ↟((↑(LinearEquiv.symm homLinearEquiv) : ((↑N : Type u) →ₗ[R] (↑P : Type u)) →ₗ[R] N ⟶ P) ∘ₗ
        LinearMap.lcomp R (↑P : Type u) (Hom.hom f) ∘ₗ
          (↑homLinearEquiv : (M ⟶ P) →ₗ[R] (↑M : Type u) →ₗ[R] (↑P : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
hf : Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
hf :
  ∀ (x : (↑X₁ : Type u)) (y : (↑X₂ : Type u)),
    Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
      ((Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) :
            (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
          (x ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
      ((Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f)) :
            (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
          (x ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
⊢ Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : (↑X₁ : Type u)
y : (↑X₂ : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
    ((Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) :
          (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
        (x ⊗ₜ[R] y) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
    ((Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f)) :
          (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
        (x ⊗ₜ[R] y) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ₘ f)

Tactic:
apply braiding_naturality

Premises used: SemimoduleCat.MonoidalCategory.braiding_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ (𝟙 X ⊗ₘ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
apply braiding_naturality

Premises used: SemimoduleCat.MonoidalCategory.braiding_naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
hf :
  Hom.hom
      (Iso.hom (α_ X Y Z) ≫
        Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫ Iso.hom (α_ Y Z X)) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom)
⊢ Iso.hom (α_ X Y Z) ≫
      Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫ Iso.hom (α_ Y Z X) =
    (X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom

Tactic:
ext : 1