-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem FG.jacobson_smul_lt {N : Submodule R M} (ne_bot : N ≠ ⊥) (fg : N.FG) :
    Ring.jacobson R • N < N

Proof state:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

case h.e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
all_goals rw [Submodule.map_top, range_subtype]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Submodule.map N.subtype (Ring.jacobson R • ⊤)

Tactic:
rw [map_smul'']

Result:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Tactic:
rw [← nontrivial_iff_ne_bot] at ne_bot

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Proof state:
case h.e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
rw [Submodule.map_top, range_subtype]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : N.FG
⊢ Ring.jacobson R • N < N

Tactic:
rw [← Module.Finite.iff_fg] at fg

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N

Tactic:
convert map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)

Result:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Submodule.map N.subtype (Ring.jacobson R • ⊤)

case h.e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Proof state:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Submodule.map N.subtype (Ring.jacobson R • ⊤)

case h.e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
on_goal 1 => rw [map_smul'']

Result:
case h.e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

case h.e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤