let P : ℕ → Prop := (fun i ↦ if hi : i < n.succ then w ⟨i, hi⟩ = 0 else False)
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)
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
⊢ ∃ k, w k = 0 ∧ Monotone (Function.update w k 1)