have nem : ((range (t + 1)).image fun i => P i).Nonempty :=
  (Nonempty.image_iff _).mpr nonempty_range_succ
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))