-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma singleton_set_smul [SMulCommClass S R M] (r : S) : ({r} : Set S) • N = r • N

Proof state:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ (DistribMulAction.toLinearMap R M r) m ∈ {r} • N

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Result:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ ∀ p ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}, (DistribMulAction.toLinearMap R M r) m ∈ p

Proof state:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
p✝ : Submodule R M
hp : p✝ ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}
⊢ (DistribMulAction.toLinearMap R M r) m ∈ p✝

Tactic:
exact hp rfl hm

Result:
no goals

Proof state:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r✝ : S
m : M
hm : m ∈ N
⊢ r✝ • m ∈ r✝ • N

Tactic:
exact ⟨m, hm, rfl⟩

Result:
no goals

Proof state:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ ∀ p ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}, (DistribMulAction.toLinearMap R M r) m ∈ p

Tactic:
intro _ hp

Result:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
p✝ : Submodule R M
hp : p✝ ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}
⊢ (DistribMulAction.toLinearMap R M r) m ∈ p✝

Proof state:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ {r} • N = r • N

Tactic:
apply set_smul_eq_of_le

Result:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N

Proof state:
case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N

Tactic:
rintro _ ⟨m, hm, rfl⟩

Result:
case le.intro.intro
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ (DistribMulAction.toLinearMap R M r) m ∈ {r} • N

Proof state:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

Tactic:
rintro _ m rfl hm

Result:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r✝ : S
m : M
hm : m ∈ N
⊢ r✝ • m ∈ r✝ • N