simp only [ge_iff_le, add_apply, smul_apply, one_apply, mul_one, Nat.sub_add_cancel (h i)]
case refine_1.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i : Fin (Nat.succ n)
⊢ w i = ((fun i => w i - w 0) + w 0 • 1) i
no goals