no goals
R : Type u_1
R₁ : Type ?u.1550580
R₂ : Type ?u.1550583
R₃ : Type ?u.1550586
R₄ : Type ?u.1550589
S : Type ?u.1550592
K : Type ?u.1550595
K₂ : Type ?u.1550598
M : Type u_2
M' : Type ?u.1550604
M₁ : Type ?u.1550607
M₂ : Type ?u.1550610
M₃ : Type ?u.1550613
M₄ : Type ?u.1550616
N : Type ?u.1550619
N₂ : Type ?u.1550622
ι : Type ?u.1550625
V : Type ?u.1550628
V₂ : Type ?u.1550631
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.1550805
sc : SemilinearMapClass F τ₁₂ M M₂
p p' : Submodule R M
h : p ≤ p'
⊢ map (Submodule.subtype p') (range (ofLe h)) = p
simp [range_ofLe, map_comap_eq, h]