no goals
R : Type ?u.1512475
R₁ : Type ?u.1512478
R₂ : Type ?u.1512481
R₃ : Type ?u.1512484
R₄ : Type ?u.1512487
S : Type ?u.1512490
K : Type u_1
K₂ : Type ?u.1512496
M : Type ?u.1512499
M' : Type ?u.1512502
M₁ : Type ?u.1512505
M₂ : Type ?u.1512508
M₃ : Type ?u.1512511
M₄ : Type ?u.1512514
N : Type ?u.1512517
N₂ : Type ?u.1512520
ι : Type ?u.1512523
V : Type u_2
V₂ : Type u_3
inst✝⁵ : Semifield K
inst✝⁴ : Semifield K₂
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
h : a ≠ 0
⊢ range (a • f) = range f
simpa only [range_eq_map] using Submodule.map_smul f _ a h