rw [smallParts]
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)