no goals
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.242912
M₂ : Type ?u.242915
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ map (mkQ p) p' = ⊤ ↔ p ⊔ p' = ⊤
simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]