R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f✝ f : M →ₗ[R] P
hf : Function.Injective ↑f
N : Submodule R M
hfn : FG (map f N)
t : Finset P
ht : span R ↑t = map f N
⊢ ↑t ⊆ range ↑f
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f✝ f : M →ₗ[R] P
hf : Function.Injective ↑f
N : Submodule R M
hfn : FG (map f N)
t : Finset P
ht : span R ↑t = map f N
⊢ map f
      (span R ↑(Finset.preimage t ↑f (_ : ∀ (x : M), x ∈ ↑f ⁻¹' ↑t → ∀ (y : M), y ∈ ↑f ⁻¹' ↑t → ↑f x = ↑f y → x = y))) =
    map f N
rw [f.map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
  Set.inter_eq_self_of_subset_left, ht]
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f✝ f : M →ₗ[R] P
hf : Function.Injective ↑f
N : Submodule R M
hfn : FG (map f N)
t : Finset P
ht : span R ↑t = map f N
⊢ map f N ≤ map f ⊤
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f✝ f : M →ₗ[R] P
hf : Function.Injective ↑f
N : Submodule R M
hfn : FG (map f N)
t : Finset P
ht : span R ↑t = map f N
⊢ ↑t ⊆ range ↑f
rw [← LinearMap.range_coe, ← span_le, ht, ← map_top]
no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f✝ f : M →ₗ[R] P
hf : Function.Injective ↑f
N : Submodule R M
hfn : FG (map f N)
t : Finset P
ht : span R ↑t = map f N
⊢ map f N ≤ map f ⊤
exact map_mono le_top