exact (h wr hwr₂ (h₁.trans hle)).trans h₁
case intro.intro.intro
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
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
h₁ : wr ≤ w'
⊢ w ≤ w'
no goals