no goals
α : Type u_3
β : Type ?u.376063
γ : Type ?u.376066
ι : Type ?u.376069
M : Type u_2
M' : Type ?u.376075
N : Type u_1
P : Type ?u.376081
G : Type ?u.376084
H : Type ?u.376087
R : Type ?u.376090
S : Type ?u.376093
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f : M → N
hf : f 0 = 0
hf' : ∀ (x y : M), f (x + y) = f x + f y
v₁ v₂ : α →₀ M
x✝ : α
⊢ ↑(mapRange f hf (v₁ + v₂)) x✝ = ↑(mapRange f hf v₁ + mapRange f hf v₂) x✝
simp only [hf', add_apply, mapRange_apply]