no goals
α : Type u_1
β : Type ?u.150191
γ : Type ?u.150194
ι : Type ?u.150197
M : Type u_2
M' : Type ?u.150203
N : Type ?u.150206
P : Type ?u.150209
G : Type ?u.150212
H : Type ?u.150215
R : Type ?u.150218
S : Type ?u.150221
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (update f a b).support = if b = 0 then erase f.support a else insert a f.support
classical
dsimp [update]; congr <;> apply Subsingleton.elim
α : Type u_1
β : Type ?u.150191
γ : Type ?u.150194
ι : Type ?u.150197
M : Type u_2
M' : Type ?u.150203
N : Type ?u.150206
P : Type ?u.150209
G : Type ?u.150212
H : Type ?u.150215
R : Type ?u.150218
S : Type ?u.150221
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (if b = 0 then erase f.support a else insert a f.support) = if b = 0 then erase f.support a else insert a f.support
α : Type u_1
β : Type ?u.150191
γ : Type ?u.150194
ι : Type ?u.150197
M : Type u_2
M' : Type ?u.150203
N : Type ?u.150206
P : Type ?u.150209
G : Type ?u.150212
H : Type ?u.150215
R : Type ?u.150218
S : Type ?u.150221
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (update f a b).support = if b = 0 then erase f.support a else insert a f.support
dsimp [update]
no goals
α : Type u_1
β : Type ?u.150191
γ : Type ?u.150194
ι : Type ?u.150197
M : Type u_2
M' : Type ?u.150203
N : Type ?u.150206
P : Type ?u.150209
G : Type ?u.150212
H : Type ?u.150215
R : Type ?u.150218
S : Type ?u.150221
inst✝² : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (if b = 0 then erase f.support a else insert a f.support) = if b = 0 then erase f.support a else insert a f.support
congr <;> apply Subsingleton.elim