have := Nat.findGreatest_is_greatest hij' (Nat.le_of_lt_succ j.2)
case neg
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) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
⊢ 1 ≤ w j
case neg
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) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = m
hj : ¬j = m
hij' : m < j
this : ¬P ↑j
⊢ 1 ≤ w j