no goals
R : Type u_1
R₁ : Type ?u.1598122
R₂ : Type ?u.1598125
R₃ : Type ?u.1598128
R₄ : Type ?u.1598131
S : Type ?u.1598134
K : Type ?u.1598137
K₂ : Type ?u.1598140
M : Type u_2
M' : Type ?u.1598146
M₁ : Type ?u.1598149
M₂ : Type u_3
M₃ : Type ?u.1598155
M₄ : Type ?u.1598158
N : Type ?u.1598161
N₂ : Type ?u.1598164
ι : Type ?u.1598167
V : Type ?u.1598170
V₂ : Type ?u.1598173
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
⊢ range (rangeRestrict f) = ⊤
simp [f.range_codRestrict _]