exact (Nat.mul_div_cancel_left' (Finset.gcd_dvd (Finset.mem_univ i))).symm
case hww'.h
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
i : Fin (Nat.succ n)
⊢ w i = (Finset.gcd Finset.univ w • fun i => w i / Finset.gcd Finset.univ w) i
no goals