simp only [Finset.mem_univ, Finset.gcd_eq_zero_iff.mp hg, zero_apply]
case h₀'.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 : g = 0
i✝ : Fin (Nat.succ n)
⊢ w i✝ = 0 i✝
no goals