α : Type u_2
β : Type ?u.176434
γ : Type ?u.176437
ι : Type ?u.176440
M : Type u_1
M' : Type ?u.176446
N : Type ?u.176449
P : Type ?u.176452
G : Type ?u.176455
H : Type ?u.176458
R : Type ?u.176461
S : Type ?u.176464
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ filter (fun x => ¬f x = 0) s = filter (fun a => ¬f a = 0) s
α : Type u_2
β : Type ?u.176434
γ : Type ?u.176437
ι : Type ?u.176440
M : Type u_1
M' : Type ?u.176446
N : Type ?u.176449
P : Type ?u.176452
G : Type ?u.176455
H : Type ?u.176458
R : Type ?u.176461
S : Type ?u.176464
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = filter (fun a => f a ≠ 0) s
dsimp [onFinset]
no goals
α : Type u_2
β : Type ?u.176434
γ : Type ?u.176437
ι : Type ?u.176440
M : Type u_1
M' : Type ?u.176446
N : Type ?u.176449
P : Type ?u.176452
G : Type ?u.176455
H : Type ?u.176458
R : Type ?u.176461
S : Type ?u.176464
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ filter (fun x => ¬f x = 0) s = filter (fun a => ¬f a = 0) s
congr