-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma mem_singleton_set_smul [SMulCommClass R S M] (r : S) (x : M) :
    x ∈ ({r} : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m

Proof state:
case mp.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 R S M
r : S
x : M
t : S
n : M
memₜ : t ∈ {r}
memₙ : n ∈ N
⊢ ∃ m ∈ N, t • n = r • m

Tactic:
aesop

Result:
no goals

Proof state:
case mp.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 R S M
r : S
x : M
t : R
n : M
mem : n ∈ {r} • N
h : ∃ m ∈ N, n = r • m
⊢ ∃ m ∈ N, t • n = r • m

Tactic:
rcases h with ⟨n, hn, rfl⟩

Result:
case mp.smul₁.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 R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ ∃ m ∈ N, t • r • n = r • m

Proof state:
case mp.add.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 R S M
r : S
x m₂ : M
mem₂ : m₂ ∈ {r} • N
h₂ : ∃ m ∈ N, m₂ = r • m
m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
⊢ ∃ m ∈ N, r • m₁ + m₂ = r • m

Tactic:
rcases h₂ with ⟨m₂, h₂, rfl⟩

Result:
case mp.add.intro.intro.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 R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ ∃ m ∈ N, r • m₁ + r • m₂ = r • m

Proof state:
case mp.zero
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 R S M
r : S
x : M
⊢ ∃ m ∈ N, 0 = r • m

Tactic:
exact ⟨0, Submodule.zero_mem _, by simp⟩

Result:
no goals

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 R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ t • n ∈ N

Tactic:
aesop

Result:
no goals

Proof state:
case mp.smul₁.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 R S M
r : S
x : M
t : R
n : M
hn : n ∈ N
mem : r • n ∈ {r} • N
⊢ ∃ m ∈ N, t • r • n = r • m

Tactic:
exact ⟨t • n, by aesop,  smul_comm _ _ _⟩

Result:
no goals

Proof state:
case mpr
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 R S M
r : S
x : M
⊢ (∃ m ∈ N, x = r • m) → x ∈ {r} • N

Tactic:
aesop

Result:
no goals

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 R S M
r : S
x : M
⊢ 0 = r • 0

Tactic:
simp

Result:
no goals

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 R S M
r : S
x : M
⊢ x ∈ {r} • N ↔ ∃ m ∈ N, x = 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
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ x ∈ {r} • N → ∃ m ∈ N, x = r • m

case mpr
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 R S M
r : S
x : M
⊢ (∃ m ∈ N, x = r • m) → x ∈ {r} • N

Proof state:
case mp.add.intro.intro.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 R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ ∃ m ∈ N, r • m₁ + r • m₂ = r • m

Tactic:
exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩

Result:
no goals

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 R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ r • m₁ + r • m₂ = r • (m₁ + m₂)

Tactic:
simp

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
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ x ∈ {r} • N → ∃ m ∈ N, x = r • m

Tactic:
intro hx

Result:
case mp
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 R S M
r : S
x : M
hx : x ∈ {r} • N
⊢ ∃ m ∈ N, x = r • m

Proof state:
case mp
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 R S M
r : S
x : M
hx : x ∈ {r} • N
⊢ ∃ m ∈ N, x = r • m

Tactic:
induction' x, hx using Submodule.set_smul_inductionOn with
  t n memₜ memₙ t n mem h m₁ m₂ mem₁ mem₂ h₁ h₂

Result:
case mp.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 R S M
r : S
x : M
t : S
n : M
memₜ : t ∈ {r}
memₙ : n ∈ N
⊢ ∃ m ∈ N, t • n = r • m

case mp.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 R S M
r : S
x : M
t : R
n : M
mem : n ∈ {r} • N
h : ∃ m ∈ N, n = r • m
⊢ ∃ m ∈ N, t • n = r • m

case mp.add
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 R S M
r : S
x m₁ m₂ : M
mem₁ : m₁ ∈ {r} • N
mem₂ : m₂ ∈ {r} • N
h₁ : ∃ m ∈ N, m₁ = r • m
h₂ : ∃ m ∈ N, m₂ = r • m
⊢ ∃ m ∈ N, m₁ + m₂ = r • m

case mp.zero
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 R S M
r : S
x : M
⊢ ∃ m ∈ N, 0 = r • m