Chore(Data/Set/Card): Remove unnecessary assumption for ncard eq of b…

…ijective (#12108)

Drop redundant hypothesis `s.Finite` from `Set.ncard_eq_of_bijective`.

Mathlib/Data/Set/Card.lean

@@ -738,12 +738,16 @@ theorem ncard_strictMono [Finite α] : @StrictMono (Set α) _ _ _ ncard :=
 
 theorem ncard_eq_of_bijective {n : ℕ} (f : ∀ i, i < n → α)
     (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a) (hf' : ∀ (i) (h : i < n), f i h ∈ s)
-    (f_inj : ∀ (i j) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j)
-    (hs : s.Finite := by toFinite_tac) :
-    s.ncard = n := by
-  rw [ncard_eq_toFinset_card _ hs]
-  apply Finset.card_eq_of_bijective
-  all_goals simpa
+    (f_inj : ∀ (i j) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) : s.ncard = n := by
+  let f' : Fin n → α := fun i ↦ f i.val i.is_lt
+  suffices himage : s = f' '' Set.univ by
+    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
+    exact ncard_image_of_injOn <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h
+  ext x
+  simp only [image_univ, mem_range]
+  refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
+  obtain ⟨i, hi, rfl⟩ := hf x hx
+  use ⟨i, hi⟩
 #align set.ncard_eq_of_bijective Set.ncard_eq_of_bijective
 
 theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha ∈ t)