English
If p is extensionally equal to a Finset s, then toFinset p computed via the corresponding fintype equals s.
Русский
Если p эквивалентно по расширению некоторому Finset s, то toFinset p, полученное через соответствующий экземпляр fintype, равно s.
LaTeX
$$$\forall p\, (s: Finset\ α)\ (H: \forall x, x \in s \iff x \in p),\; toFinset(p) = s$$$
Lean4
/-- Many `Fintype` instances for sets are defined using an extensionally equal `Finset`.
Rewriting `s.toFinset` with `Set.toFinset_ofFinset` replaces the term with such a `Finset`. -/
theorem toFinset_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) :
@Set.toFinset _ p (Fintype.ofFinset s H) = s :=
Finset.ext fun x => by rw [@mem_toFinset _ _ (id _), H]
