α : Type ?u.72269
β : Type ?u.72272
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ List.length (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)) =
    Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
α : Type ?u.72269
β : Type ?u.72272
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ Nat.Subtype.toFunAux x = Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
rw [toFunAux, List.countp_eq_length_filter]
no goals
α : Type ?u.72269
β : Type ?u.72272
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ List.length (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)) =
    Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
rfl