no goals
R : Type u_1
R₁ : Type ?u.1536535
R₂ : Type ?u.1536538
R₃ : Type ?u.1536541
R₄ : Type ?u.1536544
S : Type ?u.1536547
K : Type ?u.1536550
K₂ : Type ?u.1536553
M : Type u_2
M' : Type ?u.1536559
M₁ : Type ?u.1536562
M₂ : Type ?u.1536565
M₃ : Type ?u.1536568
M₄ : Type ?u.1536571
N : Type ?u.1536574
N₂ : Type ?u.1536577
ι : Type ?u.1536580
V : Type ?u.1536583
V₂ : Type ?u.1536586
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.1536760
sc : SemilinearMapClass F τ₁₂ M M₂
p' : Submodule R { x // x ∈ p }
⊢ map (Submodule.subtype p) p' ≤ p
simpa using (map_le_range : map p.subtype p' ≤ range p.subtype)