[GOAL]
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
[PROOFSTEP]
refine' le_antisymm _ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
[GOAL]
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
[PROOFSTEP]
intro n hn
[GOAL]
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
[PROOFSTEP]
cases' Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN with r hr
[GOAL]
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
[PROOFSTEP]
cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1) with s hs
[GOAL]
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
[PROOFSTEP]
have : n = -(s * r - 1) • n := by rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
[GOAL]
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
[PROOFSTEP]
rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
[GOAL]
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
[PROOFSTEP]
rw [this]
[GOAL]
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
[PROOFSTEP]
exact Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson ⊥
⊢ N = ⊥
[PROOFSTEP]
rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have hNN' : N ⊔ N' = N ⊔ I • N' :=
  le_antisymm hNN (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have h_comap := Submodule.comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have : (I • N').map N.mkQ = N'.map N.mkQ := by
  rw [← h_comap.eq_iff]
  simpa [comap_map_eq, sup_comm, eq_comm] using hNN'
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ map (mkQ N) (I • N') = map (mkQ N) N'
[PROOFSTEP]
rw [← h_comap.eq_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ comap (mkQ N) (map (mkQ N) (I • N')) = comap (mkQ N) (map (mkQ N) N')
[PROOFSTEP]
simpa [comap_map_eq, sup_comm, eq_comm] using hNN'
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this : map (mkQ N) (I • N') = map (mkQ N) N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have :=
  @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _) (by rw [← map_smul'', this]) hIJ
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this : map (mkQ N) (I • N') = map (mkQ N) N'
⊢ map (mkQ N) N' ≤ I • map (mkQ N) N'
[PROOFSTEP]
rw [← map_smul'', this]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this✝ : map (mkQ N) (I • N') = map (mkQ N) N'
this : map (mkQ N) N' = J • map (mkQ N) N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
rw [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm, hNN'] at this 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this✝ : map (mkQ N) (I • N') = map (mkQ N) N'
this : N ⊔ I • N' = J • N' ⊔ N
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
rw [this, sup_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson ⊥
hNN : N ⊔ N' ≤ N ⊔ I • N'
⊢ I • N' ≤ N
[PROOFSTEP]
rw [← sup_eq_left, smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
