cases this with
| inl h => 
  exfalso; exact h'.2 h
| inr h => exact h
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
this : P a = minP t P ∨ P a = minP t P + 1
⊢ P a = minP t P + 1
no goals