R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : M), n ∈ span R s → r • n = 0) ↔ ∀ (n : ↑s), r • ↑n = 0
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ r ∈ annihilator (span R s) ↔ ∀ (n : ↑s), r • ↑n = 0
rw [Submodule.mem_annihilator]
case mp
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : M), n ∈ span R s → r • n = 0) → ∀ (n : ↑s), r • ↑n = 0

case mpr
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ (n : M), n ∈ span R s → r • n = 0
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : M), n ∈ span R s → r • n = 0) ↔ ∀ (n : ↑s), r • ↑n = 0
constructor
case mp
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : M), n ∈ span R s → r • n = 0
n : ↑s
⊢ r • ↑n = 0
case mp
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : M), n ∈ span R s → r • n = 0) → ∀ (n : ↑s), r • ↑n = 0
intro h n
no goals
case mp
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : M), n ∈ span R s → r • n = 0
n : ↑s
⊢ r • ↑n = 0
exact h _ (Submodule.subset_span n.prop)
case mpr
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • n = 0
case mpr
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
⊢ (∀ (n : ↑s), r • ↑n = 0) → ∀ (n : M), n ∈ span R s → r • n = 0
intro h n hn
case mpr.refine_1
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x : M), x ∈ s → r • x = 0

case mpr.refine_2
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

case mpr.refine_3
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), r • x = 0 → r • y = 0 → r • (x + y) = 0

case mpr.refine_4
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R) (x : M), r • x = 0 → r • a • x = 0
case mpr
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • n = 0
refine Submodule.span_induction hn ?_ ?_ ?_ ?_
case mpr.refine_1
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x : M
hx : x ∈ s
⊢ r • x = 0
case mpr.refine_1
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x : M), x ∈ s → r • x = 0
intro x hx
no goals
case mpr.refine_1
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x : M
hx : x ∈ s
⊢ r • x = 0
exact h ⟨x, hx⟩
no goals
case mpr.refine_2
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0
exact smul_zero _
case mpr.refine_3
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx : r • x = 0
hy : r • y = 0
⊢ r • (x + y) = 0
case mpr.refine_3
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), r • x = 0 → r • y = 0 → r • (x + y) = 0
intro x y hx hy
no goals
case mpr.refine_3
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
x y : M
hx : r • x = 0
hy : r • y = 0
⊢ r • (x + y) = 0
rw [smul_add, hx, hy, zero_add]
case mpr.refine_4
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
a : R
x : M
hx : r • x = 0
⊢ r • a • x = 0
case mpr.refine_4
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R) (x : M), r • x = 0 → r • a • x = 0
intro a x hx
no goals
case mpr.refine_4
R : Type u
M : Type v
F : Type ?u.12996
G : Type ?u.12999
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
a : R
x : M
hx : r • x = 0
⊢ r • a • x = 0
rw [smul_comm, hx, smul_zero]