no goals
α : Type u_3
β : Type ?u.180467
γ : Type ?u.180470
ι : Type ?u.180473
M : Type u_2
M' : Type ?u.180479
N : Type u_1
P : Type ?u.180485
G : Type ?u.180488
H : Type ?u.180491
R : Type ?u.180494
S : Type ?u.180497
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ ↑(mapRange f hf (single a b)) a' = ↑(single a (f b)) a'
classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'
no goals
α : Type u_3
β : Type ?u.180467
γ : Type ?u.180470
ι : Type ?u.180473
M : Type u_2
M' : Type ?u.180479
N : Type u_1
P : Type ?u.180485
G : Type ?u.180488
H : Type ?u.180491
R : Type ?u.180494
S : Type ?u.180497
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ ↑(mapRange f hf (single a b)) a' = ↑(single a (f b)) a'
simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'