-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
@[simp] lemma empty_set_smul : (∅ : Set S) • N = ⊥

Proof state:
case h.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
x✝ : M
⊢ x✝ ∈ ∅ • N → x✝ ∈ ⊥

Tactic:
intro hx

Result:
case h.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
x✝ : M
hx : x✝ ∈ ∅ • N
⊢ x✝ ∈ ⊥

Proof state:
case h.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
x✝ : M
hx : x✝ ∈ ∅ • N
⊢ x✝ ∈ ⊥

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf] at hx

Result:
case h.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
x✝ : M
hx : ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}, x✝ ∈ p
⊢ x✝ ∈ ⊥

Proof state:
case h.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
x✝ : M
⊢ x✝ ∈ ⊥ → x✝ ∈ ∅ • N

Tactic:
rintro rfl

Result:
case h.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
⊢ 0 ∈ ∅ • N

Proof state:
case h.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
x✝ : M
hx : ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}, x✝ ∈ p
⊢ x✝ ∈ ⊥

Tactic:
exact hx ⊥ (fun r _ hr ↦ hr.elim)

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
⊢ ∅ • N = ⊥

Tactic:
ext

Result:
case h
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
x✝ : M
⊢ x✝ ∈ ∅ • N ↔ x✝ ∈ ⊥

Proof state:
case h
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
x✝ : M
⊢ x✝ ∈ ∅ • N ↔ x✝ ∈ ⊥

Tactic:
fconstructor

Result:
case h.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
x✝ : M
⊢ x✝ ∈ ∅ • N → x✝ ∈ ⊥

case h.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
x✝ : M
⊢ x✝ ∈ ⊥ → x✝ ∈ ∅ • N

Proof state:
case h.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
⊢ 0 ∈ ∅ • N

Tactic:
exact Submodule.zero_mem _

Result:
no goals