-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma set_smul_eq_map [SMulCommClass R R N] :
    sR • N =
    Submodule.map
      (N.subtype.comp (Finsupp.lsum R <| DistribMulAction.toLinearMap _ _))
      (Finsupp.supported N R sR)

Proof state:
case closed_under_smul
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
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩

Result:
no goals

Proof state:
case le
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
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • N

Tactic:
intro x hx

Result:
case le
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
x : M
hx : x ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
⊢ x ∈ sR • N

Proof state:
case le.intro.intro.refine_2.h
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)
x : M
⊢ sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N ↔ x ∈ sR • N

Tactic:
fconstructor

Result:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ (sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N) → x ∈ sR • N

case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

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
inst✝ : SMulCommClass R R ↥N
⊢ sR • N = map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

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
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N →
        r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

case le
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
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • 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
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ↑(∑ x ∈ c.support, (DistribMulAction.toLinearMap R (↥N) x) (c x)) ∈ sR • N

Tactic:
rw [AddSubmonoid.coe_finset_sum]

Result:
case le.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)
⊢ ∑ i ∈ c.support, ↑((DistribMulAction.toLinearMap R (↥N) i) (c i)) ∈ sR • N

Proof state:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ sR • N

Tactic:
rw [mem_set_smul_def, mem_sInf]

Result:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, r • n ∈ p

Proof state:
case le.intro.intro.refine_1
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)
r : R
hr : r ∈ c.support
⊢ ↑((DistribMulAction.toLinearMap R (↥N) r) (c r)) ∈ sR • N

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf]

Result:
case le.intro.intro.refine_1
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)
r : R
hr : r ∈ c.support
⊢ ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, ↑((DistribMulAction.toLinearMap R (↥N) r) (c r)) ∈ p

Proof state:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

Tactic:
aesop

Result:
no goals

Proof state:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : R⦄ {n : M}, r ∈ sR → n ∈ N → r • n ∈ p}, r • n ∈ p

Tactic:
exact fun p hp ↦ hp hr hn

Result:
no goals

Proof state:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ (sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N) → x ∈ sR • N

Tactic:
refine fun h ↦ h fun r n hr hn ↦ ?_

Result:
case le.intro.intro.refine_2.h.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
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
h : sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ sR • 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
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N →
        r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
intro r n hr hn

Result:
case closed_under_smul
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
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)