rw [ha] at hk2
case h
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
⊢ P k = minP t P
case h
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 = min' (image (fun i => P i) (range (t + 1))) nem
⊢ P k = minP t P