refine ⟨fun h w' hw' hle ↦ h _ hw'.2 hle, fun h w' hw' hle ↦ ?_⟩
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w') ↔ ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
⊢ w ≤ w'