exact hf (this h')
case neg
n d : ℕ
inst✝ : NeZero d
w w₁ : Weight n d
h : ∀ y < w₁, (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) y
hw₁n : normalized w₁
hw₁ : ∀ (w₂ : Weight n d), normalized w₂ → ¬w₂ < w₁
w' : Weight n d
hw' : normalized w'
h' : w' ≤ w₁
hf : ¬w₁ ≤ w'
this : w' ≤ w₁ → w₁ ≤ w'
⊢ False
no goals