exact hw.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
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
no goals