no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.199269
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
N : Submodule R M
h : FG N
⊢ FG (map (Submodule.subtype N) ⊤)
rwa [map_top, range_subtype]