Manipulating encard, and when to use Sets vs Finsets

Stream: general

[Teddy Baker]

I am working on a problem involving the cardinality of certain sets. Although the sets are all finite, sometimes I find it easier to use Sets because of the implicit set notation. For example, during the proof I define the following set

let S₂ : Set ℕ := {i | i ∈ Finset.Ico 25 1000 ∧ ∃ n ∈ S i, ∃ m, m * m = n}

I cannot easily define that set as a Finset. Even if I try

let S₂ : Finset ℕ := Finset.filter (fun i => ∃ n ∈ S i, ∃ m, m * m = n) (Finset.Ico 25 1000)

I get an error saying failed to synthesize instance DecidablePred fun i => ∃ n ∈ S i, ∃ m, m * m = n. I know that I could instead demand that Nat.sqrt n = n, but I'm just illustrating some of the difficulty working with Finsets.

To state the problem, which involves finding a cardinality, I use Set.encard S. I have found that despite the ease of working with the implicit set notation, I have now entered a different realm of difficulty dealing with the WithTop naturals instead of numbers. Despite my best efforts, I have not even been able to solve the following extremely simple equation

import Mathlib

open Real
open Nat
open BigOperators

theorem encard_eq (S : Set ℕ) (h : S.encard + 267 = 975) :
  S.encard = 708 := by
  sorry

Clearly, my decision to use Sets instead of Finsets has backfired.

My questions are as follows:
1.) In this type of situation, is it more common to use Finsets for everything and try to prove finiteness for every new definition. Is that a superior method?
2.) How would I prove the above equation for S.encard.
3.) I am also aware that you can use ncard which bypasses withTop, but based on some reading it looks like that might not be the preferred method either.

Any help will be greatly appreciated, thanks in advance!

[Ruben Van de Velde]

import Mathlib

open Real
open Nat
open BigOperators

theorem encard_eq (S : Set ℕ) (h : S.encard + 267 = 975) :
    S.encard = 708 := by
  lift S.encard to ℕ with N
  · intro H
    rw [H, top_add, ← cast_ofNat] at h
    exact ENat.top_ne_coe _ h
  norm_cast at h
  norm_cast
  rw [eq_tsub_of_add_eq h]

I think avoiding Finset is doing you more harm than good

[Kyle Miller]

Maybe you could work with docs#Set.ncard instead of docs#Set.encard ? Rather than using extended naturals to capture finiteness, you can use docs#Set.finite proof or a docs#Finite instance, to separate cardinality from finiteness.