simp only [Set.mem_setOf_eq] at hh hy ht
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t ∈ {w | w i = 0}
y : ι →₀ ℕ
hy : y ∈ {w | w i = 0}
hh :
  (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) t =
    (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) y
⊢ t = y
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
t : ι →₀ ℕ
ht : t i = 0
y : ι →₀ ℕ
hy : y i = 0
hh :
  t + Finsupp.single i (p.totalDegree - t.sum fun x m => m) = y + Finsupp.single i (p.totalDegree - y.sum fun x m => m)
⊢ t = y