no goals
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ : Submodule R M
R₂ : Type ?u.225550
M₂ : Type ?u.225553
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap (mkQ p) p'
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')