have ain := min'_mem ((range (t + 1)).image fun i => P i) nem
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
⊢ 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)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))