no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.1285
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]