no goals
R : Type u_1
R₂ : Type u_3
K : Type ?u.300612
M : Type u_2
M₂ : Type u_4
V : Type ?u.300621
S : Type ?u.300624
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
h : LinearMap.ker f ≤ p
⊢ comap f (map f p) = p
rw [Submodule.comap_map_eq, sup_of_le_left h]