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.36053
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
⊢ sSup {a | IsAtom a} = ⊤
simp_rw [← h, isSimpleModule_iff_isAtom]