Card filter eval subtype eq pi Finset

lemma card_filter_eval_subtype_eq_piFinset    {F : Type} [Field F] [DecidableEq F]    {s : ℕ} (S : Fin s → Set F) [∀ i, Fintype ↥(S i)]    (f : MvPolynomial (Fin s) F) :    (Finset.univ.filter (fun (x : ∀ i, ↥(S i)) =>      MvPolynomial.eval (fun i => (↑(x i) : F)) f = 0)).card =    (Finset.filter (fun x => MvPolynomial.eval x f = 0)      (Fintype.piFinset (fun i => (S i).toFinset))).card := by  refine Finset.card_bij ?_ ?_ ?_ ?_;  · use fun a ha => fun i => a i  · grind  · exact fun a₁ ha₁ a₂ ha₂ h => funext fun i => Subtype.ext <| congr_fun h i  · simp only [Finset.mem_filter, Fintype.mem_piFinset, Set.mem_toFinset, Finset.mem_univ,    true_and, exists_prop, and_imp]    exact fun b hb hb' => ⟨fun i => ⟨b i, hb i⟩, hb', rfl⟩