-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma mem_set_smul (x : M) [SMulCommClass R R N] :
    x ∈ sR • N ↔ ∃ (c : R →₀ N), (c.support : Set R) ⊆ sR ∧ x = c.sum fun r m ↦ r • m

Proof state:
case mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)) →
    ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, x ∈ p

Tactic:
rintro ⟨c, hc1, rfl⟩ p hp

Result:
case mpr.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ↑(c.sum fun r m => r • m) ∈ p

Proof state:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ x ∈ sR • N → ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Tactic:
intros h

Result:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ sR • N
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Proof state:
case mpr.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ∑ i ∈ c.support, ↑(i • c i) ∈ p

Tactic:
exact Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∃ c_1,
    ↑c_1.support ⊆ sR ∧
      (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) c = ↑(c_1.sum fun r m => r • m)

Tactic:
exact ⟨c, hc, rfl⟩

Result:
no goals

Proof state:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ sR • N
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Tactic:
rw [set_smul_eq_map] at h

Result:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Proof state:
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ x ∈ sR • N ↔ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Tactic:
fconstructor

Result:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ x ∈ sR • N → ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

case mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)) → x ∈ sR • N

Proof state:
case mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)) → x ∈ sR • N

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Result:
case mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
⊢ (∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)) →
    ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, x ∈ p

Proof state:
case mp
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)

Tactic:
obtain ⟨c, hc, rfl⟩ := h

Result:
case mp.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∃ c_1,
    ↑c_1.support ⊆ sR ∧
      (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) c = ↑(c_1.sum fun r m => r • m)

Proof state:
case mpr.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ↑(c.sum fun r m => r • m) ∈ p

Tactic:
rw [Finsupp.sum, AddSubmonoid.coe_finset_sum]

Result:
case mpr.intro.intro
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc1 : ↑c.support ⊆ sR
p : Submodule R M
hp : p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}
⊢ ∑ i ∈ c.support, ↑(i • c i) ∈ p