refine (not_in_M_of_dom_ne ⟨w', ⟨?_, ?_⟩, ?_, ?_⟩) hM
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ False
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' 0 = 0

case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone w'

case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≤ w

case refine_4
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≠ w