exact le_of_eq_of_le (hS₂.2 w₁ w hw₁ h (hle.trans hw'₂)).symm hle
case h.refine_1.intro.intro
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
h : w ∈ S
w' : Weight n d
hw'₁ : normalized w'
hw'₂ : w' ≤ w
w₁ : Weight n d
hw₁ : w₁ ∈ S
hle : w₁ ≤ w'
⊢ w ≤ w'
no goals