-- Mathlib/RingTheory/Ideal/Operations.lean
lemma coe_span_smul {R' M' : Type*} [CommSemiring R'] [AddCommMonoid M'] [Module R' M']
    (s : Set R') (N : Submodule R' M') :
    (Ideal.span s : Set R') • N = s • N :=
  set_smul_eq_of_le _ _ _
    (by rintro r n hr hn
        induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn) <|
    set_smul_mono_left _ Submodule.subset_span

Proof state:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ x✝ : R'
hr : x✝ ∈ span R' s
a✝ : x✝ • n ∈ s • N
⊢ (a✝¹ • x✝) • n ∈ s • N

Tactic:
rw [mem_span_set] at hr

Result:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ x✝ : R'
hr : ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = x✝
a✝ : x✝ • n ∈ s • N
⊢ (a✝¹ • x✝) • n ∈ s • N

Proof state:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
⊢ ∑ i ∈ c.support, (a✝¹ • c i • i) • n ∈ s • N

Tactic:
refine Submodule.sum_mem _ fun i hi => ?_

Result:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (a✝¹ • c i • i) • n ∈ s • N

Proof state:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (a✝¹ • c i • i) • n ∈ s • N

Tactic:
rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]

Result:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ i • (a✝¹ * c i) • n ∈ s • N

Proof state:
case mem
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ : R'
h : x✝ ∈ s
⊢ x✝ • n ∈ s • N

Tactic:
exact mem_set_smul_of_mem_mem h hn

Result:
no goals

Proof state:
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ ↑(Ideal.span s)
hn : n ∈ N
⊢ r • n ∈ s • N

Tactic:
induction hr using Submodule.span_induction with
| mem _ h => exact mem_set_smul_of_mem_mem h hn
| zero => rw [zero_smul]; exact Submodule.zero_mem _
| add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
| smul _ _ hr =>
  rw [mem_span_set] at hr
  obtain ⟨c, hc, rfl⟩ := hr
  rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
  refine Submodule.sum_mem _ fun i hi => ?_
  rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
  exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

Result:
no goals

Proof state:
case smul
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ x✝ : R'
hr : ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = x✝
a✝ : x✝ • n ∈ s • N
⊢ (a✝¹ • x✝) • n ∈ s • N

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

Result:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
⊢ (a✝¹ • c.sum fun mi r => r • mi) • n ∈ s • N

Proof state:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
⊢ (a✝¹ • c.sum fun mi r => r • mi) • n ∈ s • N

Tactic:
rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]

Result:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
⊢ ∑ i ∈ c.support, (a✝¹ • c i • i) • n ∈ s • N

Proof state:
case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 • n ∈ s • N

Tactic:
rw [zero_smul]

Result:
case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N

Proof state:
case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ (x✝ + y✝) • n ∈ s • N

Tactic:
rw [add_smul]

Result:
case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ x✝ • n + y✝ • n ∈ s • N

Proof state:
case zero
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ 0 ∈ s • N

Tactic:
exact Submodule.zero_mem _

Result:
no goals

Proof state:
case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ x✝ • n + y✝ • n ∈ s • N

Tactic:
exact Submodule.add_mem _ ihr ihs

Result:
no goals

Proof state:
case smul.intro.intro
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a✝¹ : R'
c : R' →₀ R'
hc : ↑c.support ⊆ s
a✝ : (c.sum fun mi r => r • mi) • n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ i • (a✝¹ * c i) • n ∈ s • N

Tactic:
exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

Result:
no goals

Proof state:
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
⊢ ∀ ⦃r : R'⦄ ⦃n : M'⦄, r ∈ ↑(Ideal.span s) → n ∈ N → r • n ∈ s • N

Tactic:
rintro r n hr hn

Result:
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ ↑(Ideal.span s)
hn : n ∈ N
⊢ r • n ∈ s • N