no goals
R : Type u_3
R₂ : Type u_2
K : Type ?u.321422
M : Type u_4
M₂ : Type u_1
V : Type ?u.321431
S : Type ?u.321434
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : range f = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ ker f = ⊤
simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]