α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries)) =
    toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries))
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (lookupFinsupp l).support = toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries))
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
case h.e_2.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b

case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries)) =
    toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries))
congr
case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
case h.e_2.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b

case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
. apply Subsingleton.elim
no goals
case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
. funext ; congr
no goals
case h.e_2.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b
apply Subsingleton.elim
case h.e_3.h.e_a.e_p.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
x✝ : (_ : α) × M
⊢ (decide ¬x✝.snd = 0) = decide ¬x✝.snd = 0
case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
funext
no goals
case h.e_3.h.e_a.e_p.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
x✝ : (_ : α) × M
⊢ (decide ¬x✝.snd = 0) = decide ¬x✝.snd = 0
congr