no goals
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = Finset.erase f.support a
classical
dsimp [erase]
congr; apply Subsingleton.elim
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ Finset.erase f.support a = Finset.erase f.support a
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (erase a f).support = Finset.erase f.support a
dsimp [erase]
case h.e_2.h
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ Finset.erase f.support a = Finset.erase f.support a
congr
no goals
case h.e_2.h
α : Type u_1
β : Type ?u.162373
γ : Type ?u.162376
ι : Type ?u.162379
M : Type u_2
M' : Type ?u.162385
N : Type ?u.162388
P : Type ?u.162391
G : Type ?u.162394
H : Type ?u.162397
R : Type ?u.162400
S : Type ?u.162403
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
f : α →₀ M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝ a b
apply Subsingleton.elim