Auxiliary lemmas for multivariate polynomials

theorem List.distinct_of_inj_nodup {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} (h₁ : Function.Injective f) (h₂ : l.Nodup) : Pairwise (fun (a b : α) => f a ≠ f b) l

theorem Option.filter_irrel {α : Type} {o : Option α} {p : α → Bool} (h : ∀ (x : α), x ∈ o → p x = true) : Option.filter p o = o