no goals
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
rw [← sup_eq_left, smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul,
  sup_bot_eq]