constructor
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) →
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))

case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) →
    a ∈ range (t + 1)