R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
⊢ N ≤ J • N
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
⊢ N = J • N
refine' le_antisymm _ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
⊢ n ∈ J • N
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
⊢ N ≤ J • N
intro n hn
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
⊢ n ∈ J • N
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
⊢ n ∈ J • N
cases' Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN with r hr
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n ∈ J • N
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
⊢ n ∈ J • N
cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1) with s hs
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ n ∈ J • N
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n ∈ J • N
have : n = -(s * r - 1) • n := by
  rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ -(s * r - 1) • n ∈ J • N
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ n ∈ J • N
rw [this]
no goals
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ -(s * r - 1) • n ∈ J • N
exact Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn
no goals
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = -(s * r - 1) • n
rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]