no goals
α : Type u_1
β : Type ?u.41852
γ : Type ?u.41855
ι : Type ?u.41858
M : Type u_2
M' : Type ?u.41864
N : Type ?u.41867
P : Type ?u.41870
G : Type ?u.41873
H : Type ?u.41876
R : Type ?u.41879
S : Type ?u.41882
inst✝¹ : Zero M
a✝ a' : α
b✝ : M
inst✝ : DecidableEq α
a : α
b : M
⊢ ↑(single a b) = update 0 a b
classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]
no goals
α : Type u_1
β : Type ?u.41852
γ : Type ?u.41855
ι : Type ?u.41858
M : Type u_2
M' : Type ?u.41864
N : Type ?u.41867
P : Type ?u.41870
G : Type ?u.41873
H : Type ?u.41876
R : Type ?u.41879
S : Type ?u.41882
inst✝¹ : Zero M
a✝ a' : α
b✝ : M
inst✝ : DecidableEq α
a : α
b : M
⊢ ↑(single a b) = update 0 a b
rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]