awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
refine_1 : (e : (a : Unit) → ℕ) () ≤ #S
⊢ ∃ e ≤ #S, m = single i e
have refine_2 : m = single i ((e : (a : Unit) → ℕ) ())
Tactic: refine ⟨e (), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
have refine_1 : LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
  ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)
Tactic: suffices e ≼[lex] single () #S by
      simpa [MonomialOrder.lex_le_iff_of_unique] using this
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
⊢ LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)
have refine_1 : LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
  ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (MonomialOrder.degree lex (P S ())) : syn (σ := Unit) lex)
Tactic: rw [← Alon.degree_P]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
refine_1 :
  LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (MonomialOrder.degree lex (P S ())) : syn (σ := Unit) lex)
⊢ LE.le (α := syn (σ := Unit) lex) ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) e : syn (σ := Unit) lex)
    ((toSyn lex : (a : Unit →₀ ℕ) → lex.syn) (single () #S) : syn (σ := Unit) lex)
have refine_1₁ : MonomialOrder Unit
Tactic: rw [← Alon.degree_P]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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 ∈ support (P S ())
have refine_1 : coeff e (P S ()) ≠ 0
Tactic: rw [mem_support_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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) → ℕ) ())
have refine_2 : Eq.{u_3 + 1} (α := ι →₀ ℕ) (mapDomain (fun (x : Unit) ↦ i) e) (single i ((e : (a : Unit) → ℕ) ()))
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
⊢ Eq.{u_3 + 1} (α := ι →₀ ℕ) (mapDomain (fun (x : Unit) ↦ i) e) (single i ((e : (a : Unit) → ℕ) ()))
have refine_2 : ∀ (j : ι),
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have pos : ∀ (hj : j = i),
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
pos :
  ∀ (hj : j = i),
    Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
      (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have neg : ∀ (hj : ¬j = i),
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
hj : j = i
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have pos : Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) i : ℕ)
  (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
Tactic: rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
hj : j = i
pos :
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) i : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have pos₁ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
Tactic: rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
hj : j = i
pos :
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) i : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
pos₁ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have pos₂ : Unit
Tactic: rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
hj : j = i
pos :
  Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) i : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
pos₁ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
pos₂ : Unit
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have pos₃ : Eq (α := ℕ) ((e : (a : Unit) → ℕ) () : ℕ) ((e : (a : Unit) → ℕ) () : ℕ)
Tactic: rw [hj, mapDomain_apply (Function.injective_of_subsingleton _), single_eq_same]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
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
j : ι
hj : ¬j = i
⊢ Eq (α := ℕ) ((mapDomain (fun (x : Unit) ↦ i) e : (a : ι) → ℕ) j : ℕ)
    (((single i ((e : (a : Unit) → ℕ) ()) : ι →₀ ℕ) : (a : ι) → ℕ) j : ℕ)
have neg : j ∉ Set.range fun (x : Unit) ↦ i
Tactic: rw [mapDomain_notin_range, single_eq_of_ne hj]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ support (P S i)
⊢ ∃ e ≤ #S, m = single i e
have have : Eq (α := MvPolynomial ι R) (P S i) ((rename fun (x : Unit) ↦ i : (a : MvPolynomial Unit R) → MvPolynomial ι R) (P S ()))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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 ()))
⊢ ∃ e ≤ #S, m = single i e
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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ ∃ e ≤ #S, m = single i e
have 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
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]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ ∃ e ≤ #S, m = single i e
have 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
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]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ ∃ e ≤ #S, m = single i e
have 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
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]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
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
⊢ ∃ e ≤ #S, m = single i e
have 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
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]
Cleared hypotheses: hm