-- Module: Mathlib.Combinatorics.Nullstellensatz
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
have :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
have₁ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₂ :
  Eq (α := MvPolynomial ι R) (P S i)
    ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
have₃ have₄ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₅ :
  ∀ (hm : Membership.mem (γ := Finset (ι →₀ ℕ)) (Finset.image (mapDomain fun (x : Unit) ↦ i) (support (P S ()))) m)
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))),
    ∃ e ≤ #S, m = single i e
have₆ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (hm : ∃ (a : Unit →₀ ℕ), ¬coeff a (P S ()) = 0 ∧ mapDomain (fun (x : Unit) ↦ i) a = m), ∃ e ≤ #S, m = single i e
have₇ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m), ∃ e ≤ #S, m = single i e
have₈ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m) (this : Nontrivial R),
    ∃ e ≤ #S, m = single i e
refine_1 :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m) (this : Nontrivial R),
    (e : (a : Unit) → ℕ) () ≤ #S
refine_2 refine_2₁ :
  ∀
    (hP :
      Eq (α := MvPolynomial ι R) (P S i)
        ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ())))
    (e : Unit →₀ ℕ) (he : ¬coeff e (P S ()) = 0) (hm : mapDomain (fun (x : Unit) ↦ i) e = m) (this : Nontrivial R),
    m = single i ((e : (a : Unit) → ℕ) ())
⊢ ∃ e ≤ #S, m = single i e

Tactic:
classical
  have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P]
  rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm
  simp only [Finset.mem_image, mem_support_iff, ne_eq] at hm
  obtain ⟨e, he, hm⟩ := hm
  haveI : Nontrivial R := nontrivial_of_ne _ _ he
  refine ⟨e (), ?_, ?_⟩
  · suffices e ≼[lex] single () #S by
      simpa [MonomialOrder.lex_le_iff_of_unique] using this
    rw [← Alon.degree_P]
    apply MonomialOrder.le_degree
    rw [mem_support_iff]
    convert! he
  · rw [← hm]
    ext j
    by_cases hj : j = i
    · rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
    · rw [mapDomain_notin_range, single_eq_of_ne hj]
      simp [Set.range_const, Set.mem_singleton_iff, hj]

Premises used: Finsupp.single_eq_same, MvPolynomial.mem_support_iff, Finset.mem_image, MonomialOrder.le_degree, MvPolynomial.support_rename_of_injective, Function.injective_of_subsingleton, ne_eq, Finsupp.mapDomain_apply, Set.mem_singleton_iff, Set.range_const, _private.0.MvPolynomial.Alon.degree_P, Finsupp.mapDomain_notin_range