refine WellFoundedLT.induction (α := Weight n d)
  (C := fun w ↦ normalized w → ∃ w', w' ∈ M n d ∧ w' ≤ w) w (fun w₁ h ↦ ?_)
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ normalized w → ∃ w' ∈ M n d, 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
⊢ (fun w => normalized w → ∃ w' ∈ M n d, w' ≤ w) w₁