no goals
α : Type u_3
β : Type ?u.422976
γ : Type ?u.422979
ι : Type ?u.422982
M : Type ?u.422985
M' : Type ?u.422988
N : Type ?u.422991
P : Type ?u.422994
G : Type u_1
H : Type u_2
R : Type ?u.423003
S : Type ?u.423006
inst✝¹ : NegZeroClass G
inst✝ : NegZeroClass H
f : G → H
hf : f 0 = 0
hf' : ∀ (x : G), f (-x) = -f x
v : α →₀ G
x✝ : α
⊢ ↑(mapRange f hf (-v)) x✝ = ↑(-mapRange f hf v) x✝
simp only [hf', neg_apply, mapRange_apply]