simp only [hm, dif_pos]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
m : ℕ
hm : m < Nat.succ n
⊢ P m ↔ w { val := m, isLt := hm } = 0
no goals