exact eq_of_dom_and_min' (hS₁ w' hw'₁) hw₁ (hw₂ w' (hS₁ w' hw'₁) hw'₂)
                         (fun u hu₁ hu₂ ↦ hw'₂.trans (hw₂ u hu₁ (hu₂.trans hw'₂)))
case heq
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
⊢ w' = w
no goals