have hww'i i : w i = g * w' i := congrFun hww' i
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'
⊢ False
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