exact heq ▸ hw'₁
case h.refine_2.intro.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
hw₁ : normalized w
hw₂ : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw'₁ : w' ∈ S
hw'₂ : w' ≤ w
heq : w' = w
⊢ w ∈ S
no goals