no goals
α : Type u_2
β : Type ?u.40853
γ : Type ?u.40856
ι : Type ?u.40859
M : Type u_1
M' : Type ?u.40865
N : Type ?u.40868
P : Type ?u.40871
G : Type ?u.40874
H : Type ?u.40877
R : Type ?u.40880
S : Type ?u.40883
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) a = b
classical exact Pi.single_eq_same (f := λ _ => M) a b
no goals
α : Type u_2
β : Type ?u.40853
γ : Type ?u.40856
ι : Type ?u.40859
M : Type u_1
M' : Type ?u.40865
N : Type ?u.40868
P : Type ?u.40871
G : Type ?u.40874
H : Type ?u.40877
R : Type ?u.40880
S : Type ?u.40883
inst✝ : Zero M
a a' : α
b : M
⊢ ↑(single a b) a = b
exact Pi.single_eq_same (f := λ _ => M) a b