obtain ⟨k, hk1, hk2⟩ := ain
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 : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
case intro.intro
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))