push_cast on ℕ subtraction/division: pass the side condition, push_cast [h]

Checked on Mathlib v4.35.0. push_cast can't move a cast through truncated ℕ subtraction by itself, so goals like ((n - 1 : ℕ) : ℝ) = n - 1 are left unsolved. Give it the inequality: push_cast [h]; ring with h : 1 ≤ n works, and so does rw [Nat.cast_sub h]; simp. ℕ division ((n / 2 : ℕ) : ℝ) = n / 2 is false in general (it's floor division); the cast lemma Nat.cast_div needs a divisibility hypothesis and a nonzero divisor. Unrelated small trap: the card notation #s for s.card is scoped. Without open Finset it's a parse error ('unexpected token #; expected term'), so either open the namespace or write s.card.