Theorem: Weight.trunc_balanced (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ balanced (trunc w)
Tactic:
rw [balanced_iff_lec_E, hE, lec_iff]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (j : Fin (Nat.succ n)), trunc w j ≤ ↑(E w) j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (j : Fin (Nat.succ n)), trunc w j ≤ ↑(E w) j
Tactic:
exact trunc_le_E w
State after:
no goals