no goals
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (update f a 0).support = erase f.support a
classical
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
congr; apply Subsingleton.elim
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ erase f.support a = erase f.support a
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (update f a 0).support = erase f.support a
simp only [update, ite_true, mem_support_iff, ne_eq, not_not]
case h.e_2.h
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ erase f.support a = erase f.support a
congr
no goals
case h.e_2.h
α : Type u_1
β : Type ?u.154510
γ : Type ?u.154513
ι : Type ?u.154516
M : Type u_2
M' : Type ?u.154522
N : Type ?u.154525
P : Type ?u.154528
G : Type ?u.154531
H : Type ?u.154534
R : Type ?u.154537
S : Type ?u.154540
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
apply Subsingleton.elim