refine ⟨fun h ↦ ⟨hS₁ w h, fun w' hw'₁ hw'₂ ↦ ?_⟩, fun h ↦ ?_⟩
case h
n d : ℕ
inst✝ : NeZero d
S : Set (Weight n d)
hS₁ : ∀ w ∈ S, normalized w
hS₂ : minimal_complete_set S
w : Weight n d
⊢ w ∈ S ↔ w ∈ M n d
case h.refine_1
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 ≤ w'

case h.refine_2
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 ∈ M n d
⊢ w ∈ S