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.47667
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ 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.47667
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSemisimpleModule R M → sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
intro
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.47667
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
exact IsSemisimpleModule.sSup_simples_eq_top