feat(Finset): toFinset + nontrivial (#21695)

We add simp lemmas for nontriviality with `Set.Finite.toFinset` and `Set.toFinset`.

Author: apnelson1

Mathlib/Data/Fintype/Basic.lean

@@ -668,6 +668,10 @@ alias ⟨_, toFinset_strict_mono⟩ := toFinset_ssubset_toFinset
 theorem disjoint_toFinset [Fintype s] [Fintype t] :
     Disjoint s.toFinset t.toFinset ↔ Disjoint s t := by simp only [← disjoint_coe, coe_toFinset]
 
+@[simp]
+theorem toFinset_nontrivial [Fintype s] : s.toFinset.Nontrivial ↔ s.Nontrivial := by
+  rw [Finset.Nontrivial, coe_toFinset]
+
 section DecidableEq
 
 variable [DecidableEq α] (s t) [Fintype s] [Fintype t]

Mathlib/Data/Set/Finite/Basic.lean

@@ -216,6 +216,10 @@ protected theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) (
   ext
   simp
 
+@[simp]
+protected theorem toFinset_nontrivial (h : s.Finite) : h.toFinset.Nontrivial ↔ s.Nontrivial := by
+  rw [Finset.Nontrivial, h.coe_toFinset]
+
 end Finite
 
 /-! ### Fintype instances