no goals
α : Type u_3
β : Type ?u.178673
γ : Type ?u.178676
ι : Type ?u.178679
M : Type u_2
M' : Type ?u.178685
N : Type u_1
P : Type ?u.178691
G : Type ?u.178694
H : Type ?u.178697
R : Type ?u.178700
S : Type ?u.178703
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
⊢ ↑(mapRange f hf 0) a = ↑0 a
simp only [hf, zero_apply, mapRange_apply]