no goals
R : Type u_1
R₁ : Type ?u.1541683
R₂ : Type ?u.1541686
R₃ : Type ?u.1541689
R₄ : Type ?u.1541692
S : Type ?u.1541695
K : Type ?u.1541698
K₂ : Type ?u.1541701
M : Type u_2
M' : Type ?u.1541707
M₁ : Type ?u.1541710
M₂ : Type ?u.1541713
M₃ : Type ?u.1541716
M₄ : Type ?u.1541719
N : Type ?u.1541722
N₂ : Type ?u.1541725
ι : Type ?u.1541728
V : Type ?u.1541731
V₂ : Type ?u.1541734
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p✝ p'✝ : Submodule R M
q : Submodule R₂ M₂
τ₁₂ : R →+* R₂
F : Type ?u.1541908
sc : SemilinearMapClass F τ₁₂ M M₂
p p' : Submodule R M
⊢ map (Submodule.subtype p) ⊤ ≤ p' ↔ p ≤ p'
rw [map_subtype_top]