[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
x✝ :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ 0 • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [zero_smul] using p.zero_mem
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
a : A
b : B
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ a ⊗ₜ[R] b • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [TensorProduct.Algebra.smul_def] using hA a (hB b hm)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz :
  m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier →
    z • m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
hw :
  m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier →
    w • m ∈
      {
            toAddSubsemigroup :=
              { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
            zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
hm :
  m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
⊢ (z + w) • m ∈
    {
          toAddSubsemigroup :=
            { carrier := ↑p, add_mem' := (_ : ∀ {a b : M}, a ∈ p.carrier → b ∈ p.carrier → a + b ∈ p.carrier) },
          zero_mem' := (_ : 0 ∈ p.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa only [add_smul] using p.add_mem (hz hm) (hw hm)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p
[PROOFSTEP]
suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = a ⊗ₜ[R] 1 • m
⊢ a • m ∈ p
[PROOFSTEP]
exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m = a ⊗ₜ[R] 1 • m
[PROOFSTEP]
simp [TensorProduct.Algebra.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p
[PROOFSTEP]
suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = 1 ⊗ₜ[R] b • m
⊢ b • m ∈ p
[PROOFSTEP]
exact this.symm ▸ p.smul_mem _ hm
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m = 1 ⊗ₜ[R] b • m
[PROOFSTEP]
simp [TensorProduct.Algebra.smul_def]
