awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
refine_2 :
  ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom (0 ▷ X)) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom 0) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) Y X) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (Hom.hom (0 ▷ X)) (Hom.hom 0)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
x : (↑Y : Type u)
y : (↑X : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom (0 ▷ X)) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom 0) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))

Tactic:
simp [ModuleCat.hom_whiskerRight]

Premises used: ModuleCat.hom_whiskerRight
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
refine_3 :
  Hom.hom (X ◁ (f + g)) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g))
⊢ X ◁ (f + g) =
    HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
⊢ Hom.hom (X ◁ (f + g)) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g))

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
refine_3 :
  ∀ (x : (↑X : Type u)) (y : (↑Y : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom (X ◁ (f + g))) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u))
                      (Hom.hom
                        (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z)
                          (X ◁ f) (X ◁ g))) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
⊢ Hom.hom (X ◁ (f + g)) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g))

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                    TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom (X ◁ (f + g))) :
                  (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
              x :
            (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
          (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                    TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u))
                    (Hom.hom
                      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z)
                        (X ◁ f) (X ◁ g))) :
                  (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
              x :
            (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
          (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))

Tactic:
simp [ModuleCat.hom_whiskerLeft]

Premises used: ModuleCat.hom_whiskerLeft
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
refine_4 :
  Hom.hom ((f + g) ▷ X) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X))
⊢ (f + g) ▷ X =
    HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
⊢ Hom.hom ((f + g) ▷ X) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X))

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
refine_4 :
  ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom ((f + g) ▷ X)) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u))
                      (Hom.hom
                        (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X)
                          (f ▷ X) (g ▷ X))) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
⊢ Hom.hom ((f + g) ▷ X) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X))

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
x : (↑Y : Type u)
y : (↑X : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom ((f + g) ▷ X)) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u))
                    (Hom.hom
                      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X)
                        (f ▷ X) (g ▷ X))) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))

Tactic:
simp [ModuleCat.hom_whiskerRight]

Premises used: ModuleCat.hom_whiskerRight
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
⊢ MonoidalLinear R (ModuleCat R)

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.MonoidalLinear.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
refine_1 :
  ∀ (X : ModuleCat R) {Y Z : ModuleCat R} (r : R) (f : Y ⟶ Z),
    X ◁ (r • f) =
      HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f)
refine_2 :
  ∀ (r : R) {Y Z : ModuleCat R} (f : Y ⟶ Z) (X : ModuleCat R),
    (r • f) ▷ X =
      HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X)
⊢ MonoidalLinear R (ModuleCat R)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
refine_1 :
  Hom.hom (X ◁ (r • f)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))
⊢ X ◁ (r • f) =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
⊢ Hom.hom (X ◁ (r • f)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
refine_1 :
  ∀ (x : (↑X : Type u)) (y : (↑Y : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom (X ◁ (r • f))) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u))
                      (Hom.hom
                        (HSMul.hSMul (β :=
                          tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
⊢ Hom.hom (X ◁ (r • f)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
x : (↑X : Type u)
y : (↑Y : Type u)
refine_1 :
  x ⊗ₜ[R]
      (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))
        y =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) r
      (x ⊗ₜ[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))
            y :
        TensorProduct R (↑X : Type u) (↑Z : Type u))
⊢ (Hom.hom (X ◁ (r • f)) : (a : TensorProduct R (↑X : Type u) (↑Y : Type u)) → (↑(X ⊗ Z) : Type u)) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) r
      ((Hom.hom (X ◁ f) : (a : TensorProduct R (↑X : Type u) (↑Y : Type u)) → (↑(X ⊗ Z) : Type u)) (x ⊗ₜ[R] y) :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))

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

Premises used: ModuleCat.MonoidalCategory.whiskerLeft_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ x ⊗ₜ[R]
      (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))
        y =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) r
      (x ⊗ₜ[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))
            y :
        TensorProduct R (↑X : Type u) (↑Z : Type u))

Tactic:
simp
-- 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
refine_2 :
  Hom.hom ((r • f) ▷ X) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))
⊢ (r • f) ▷ X =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X)

Tactic:
ext : 1
-- 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
⊢ Hom.hom ((r • f) ▷ X) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- 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
refine_2 :
  ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom ((r • f) ▷ X)) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                      TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u))
                      (Hom.hom
                        (HSMul.hSMul (β :=
                          tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))) :
                    (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                  (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
                x :
              (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
            (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
⊢ Hom.hom ((r • f) ▷ X) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext