no goals
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (update f a b).support = insert a f.support
classical
simp only [update, h, ite_false, mem_support_iff, ne_eq]
congr; apply Subsingleton.elim
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ insert a f.support = insert a f.support
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (update f a b).support = insert a f.support
simp only [update, h, ite_false, mem_support_iff, ne_eq]
case h.e_3.h.h.e_2.h
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ insert a f.support = insert a f.support
congr
no goals
case h.e_3.h.h.e_2.h
α : Type u_1
β : Type ?u.155949
γ : Type ?u.155952
ι : Type ?u.155955
M : Type u_2
M' : Type ?u.155961
N : Type ?u.155964
P : Type ?u.155967
G : Type ?u.155970
H : Type ?u.155973
R : Type ?u.155976
S : Type ?u.155979
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
h : b ≠ 0
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
apply Subsingleton.elim