R : Type u_2
inst✝⁵ : Ring R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type ?u.40765
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsAtom m} = ⊤
R : Type u_2
inst✝⁵ : Ring R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type ?u.40765
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
simp_rw [isSimpleModule_iff_isAtom]
no goals
R : Type u_2
inst✝⁵ : Ring R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type ?u.40765
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsAtom m} = ⊤
exact sSup_atoms_eq_top