by_cases hw₁ : ∃ w₂ : Weight n d, w₂.normalized ∧ w₂ < w₁
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₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁
case pos
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₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁

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₂, normalized w₂ ∧ w₂ < w₁
⊢ ∃ w' ∈ M n d, w' ≤ w₁