From 67e53ae5f3f2c4b2a8b99377bf23b894b6db38cd Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 21:14:46 -0400
Subject: [PATCH 01/12] remove unused config object

---
 Mathlib/Tactic/LinearCombination.lean | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/Mathlib/Tactic/LinearCombination.lean b/Mathlib/Tactic/LinearCombination.lean
index cb211e2e0e66e..b13bef32c0812 100644
--- a/Mathlib/Tactic/LinearCombination.lean
+++ b/Mathlib/Tactic/LinearCombination.lean
@@ -106,20 +106,6 @@ partial def expandLinearCombo (stx : Syntax.Term) : TermElabM (Option Syntax.Ter
     some <$> e.toSyntax
   return result.map fun r => ⟨r.raw.setInfo (SourceInfo.fromRef stx true)⟩
 
-/-- A configuration object for `linear_combination`. -/
-structure Config where
-  /-- whether or not the normalization step should be used -/
-  normalize := true
-  /-- whether to make separate subgoals for both sides or just one for `lhs - rhs = 0` -/
-  twoGoals := false
-  /-- the tactic used for normalization when checking
-  if the weighted sum is equivalent to the goal (when `normalize` is `true`). -/
-  normTac : Syntax.Tactic := Unhygienic.run `(tactic| ring_nf)
-  deriving Inhabited
-
-/-- Function elaborating `LinearCombination.Config` -/
-declare_config_elab elabConfig Config
-
 theorem eq_trans₃ (p : (a:α) = b) (p₁ : a = a') (p₂ : b = b') : a' = b' := p₁ ▸ p₂ ▸ p
 
 theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) : a' = b' := by

From acbdf9156a0497b607d0268bd88a41d3808db29d Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 21:43:33 -0400
Subject: [PATCH 02/12] add exp option to linear_combination

---
 Mathlib/Tactic/LinearCombination.lean | 26 ++++++++++++++++++++------
 test/linear_combination.lean          | 22 ++++++++++++++++++++++
 2 files changed, 42 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Tactic/LinearCombination.lean b/Mathlib/Tactic/LinearCombination.lean
index b13bef32c0812..9c62517f06dc6 100644
--- a/Mathlib/Tactic/LinearCombination.lean
+++ b/Mathlib/Tactic/LinearCombination.lean
@@ -111,9 +111,14 @@ theorem eq_trans₃ (p : (a:α) = b) (p₁ : a = a') (p₂ : b = b') : a' = b' :
 theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) : a' = b' := by
   rw [← sub_eq_zero] at p ⊢; rwa [sub_eq_zero, p] at H
 
+theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b)
+  (H : (a' - b')^n - (a - b) = 0) :
+  a' = b' := by
+  rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H
+
 /-- Implementation of `linear_combination` and `linear_combination2`. -/
 def elabLinearCombination
-    (norm? : Option Syntax.Tactic) (input : Option Syntax.Term)
+    (norm? : Option Syntax.Tactic) (exp? : Option Syntax.NumLit) (input : Option Syntax.Term)
     (twoGoals := false) : Tactic.TacticM Unit := Tactic.withMainContext do
   let p ← match input with
   | none => `(Eq.refl 0)
@@ -122,13 +127,18 @@ def elabLinearCombination
     | none => `(Eq.refl $e)
     | some p => pure p
   let norm := norm?.getD (Unhygienic.run `(tactic| ring1))
-  Tactic.evalTactic <|← withFreshMacroScope <| if twoGoals then
+  Tactic.evalTactic <| ← withFreshMacroScope <|
+  if twoGoals then
     `(tactic| (
       refine eq_trans₃ $p ?a ?b
       case' a => $norm:tactic
       case' b => $norm:tactic))
   else
-    `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
+    match exp? with
+    | some n =>
+      if n.getNat = 1 then `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
+      else `(tactic| (refine eq_of_add_pow $n $p ?a; case' a => $norm:tactic))
+    | _ => `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
 
 /--
 The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for
@@ -137,6 +147,8 @@ to get subgoals from `linear_combination` or with `skip` to disable normalizatio
 -/
 syntax normStx := atomic(" (" &"norm" " := ") withoutPosition(tactic) ")"
 
+syntax expStx := atomic(" (" &"exp" " := ") withoutPosition(num) ")"
+
 /--
 `linear_combination` attempts to simplify the target by creating a linear combination
   of a list of equalities and subtracting it from the target.
@@ -204,11 +216,13 @@ example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by
   linear_combination 3 * h a b + hqc
 ```
 -/
-syntax (name := linearCombination) "linear_combination" (normStx)? (ppSpace colGt term)? : tactic
+syntax (name := linearCombination) "linear_combination"
+  (normStx)? (expStx)? (ppSpace colGt term)? : tactic
 elab_rules : tactic
-  | `(tactic| linear_combination $[(norm := $tac)]? $(e)?) => elabLinearCombination tac e
+  | `(tactic| linear_combination $[(norm := $tac)]? $[(exp := $n)]? $(e)?) =>
+    elabLinearCombination tac n e
 
 @[inherit_doc linearCombination]
 syntax "linear_combination2" (normStx)? (ppSpace colGt term)? : tactic
 elab_rules : tactic
-  | `(tactic| linear_combination2 $[(norm := $tac)]? $(e)?) => elabLinearCombination tac e true
+  | `(tactic| linear_combination2 $[(norm := $tac)]? $(e)?) => elabLinearCombination tac none e true
diff --git a/test/linear_combination.lean b/test/linear_combination.lean
index 7a056666b3eb4..9b8fffc6b2b99 100644
--- a/test/linear_combination.lean
+++ b/test/linear_combination.lean
@@ -197,6 +197,28 @@ example (a b : ℤ) (x y : ℝ) (hab : a = b) (hxy : x = y) : 2 * x = 2 * y := b
   fail_if_success linear_combination 2 * hab
   linear_combination 2 * hxy
 
+/-! ### Cases with exponent -/
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := by
+  linear_combination (exp := 2) (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : y*z = -x := by
+  linear_combination (norm := skip) (exp := 2) (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2
+  ring
+
+example (K : Type)
+  [Field K]
+  [CharZero K]
+  {x y z : K}
+  (h₂ : y ^ 3 + x * (3 * z ^ 2) = 0)
+  (h₁ : x ^ 3 + z * (3 * y ^ 2) = 0)
+  (h₀ : y * (3 * x ^ 2) + z ^ 3 = 0)
+  (h : x ^ 3 * y + y ^ 3 * z + z ^ 3 * x = 0) :
+  x = 0 := by
+  linear_combination (exp := 6) 2 * y * z ^ 2 * h₂ / 7 + (x ^ 3  - y ^ 2 * z / 7) * h₁ -
+    x * y * z * h₀ + y * z * h / 7
+
+
 /-! ### Regression tests -/
 
 def g (a : ℤ) : ℤ := a ^ 2

From 400655056cb0a447948268a0c6a6d142400b523f Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 21:57:29 -0400
Subject: [PATCH 03/12] fix style lint

---
 Mathlib/Tactic/LinearCombination.lean |  3 +--
 test/linear_combination.lean          | 16 ++++++++--------
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Tactic/LinearCombination.lean b/Mathlib/Tactic/LinearCombination.lean
index 9c62517f06dc6..35fda273408fd 100644
--- a/Mathlib/Tactic/LinearCombination.lean
+++ b/Mathlib/Tactic/LinearCombination.lean
@@ -112,8 +112,7 @@ theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) :
   rw [← sub_eq_zero] at p ⊢; rwa [sub_eq_zero, p] at H
 
 theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b)
-  (H : (a' - b')^n - (a - b) = 0) :
-  a' = b' := by
+    (H : (a' - b')^n - (a - b) = 0) : a' = b' := by
   rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H
 
 /-- Implementation of `linear_combination` and `linear_combination2`. -/
diff --git a/test/linear_combination.lean b/test/linear_combination.lean
index 9b8fffc6b2b99..55e5adab860ed 100644
--- a/test/linear_combination.lean
+++ b/test/linear_combination.lean
@@ -207,14 +207,14 @@ example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : y*z = -x := by
   ring
 
 example (K : Type)
-  [Field K]
-  [CharZero K]
-  {x y z : K}
-  (h₂ : y ^ 3 + x * (3 * z ^ 2) = 0)
-  (h₁ : x ^ 3 + z * (3 * y ^ 2) = 0)
-  (h₀ : y * (3 * x ^ 2) + z ^ 3 = 0)
-  (h : x ^ 3 * y + y ^ 3 * z + z ^ 3 * x = 0) :
-  x = 0 := by
+    [Field K]
+    [CharZero K]
+    {x y z : K}
+    (h₂ : y ^ 3 + x * (3 * z ^ 2) = 0)
+    (h₁ : x ^ 3 + z * (3 * y ^ 2) = 0)
+    (h₀ : y * (3 * x ^ 2) + z ^ 3 = 0)
+    (h : x ^ 3 * y + y ^ 3 * z + z ^ 3 * x = 0) :
+    x = 0 := by
   linear_combination (exp := 6) 2 * y * z ^ 2 * h₂ / 7 + (x ^ 3  - y ^ 2 * z / 7) * h₁ -
     x * y * z * h₀ + y * z * h / 7
 

From 5278e4d15f810e6eded64893ed33f5b2d88ef0a3 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 22:02:29 -0400
Subject: [PATCH 04/12] update docs

---
 Mathlib/Tactic/LinearCombination.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Mathlib/Tactic/LinearCombination.lean b/Mathlib/Tactic/LinearCombination.lean
index 35fda273408fd..223777aa138ad 100644
--- a/Mathlib/Tactic/LinearCombination.lean
+++ b/Mathlib/Tactic/LinearCombination.lean
@@ -146,6 +146,10 @@ to get subgoals from `linear_combination` or with `skip` to disable normalizatio
 -/
 syntax normStx := atomic(" (" &"norm" " := ") withoutPosition(tactic) ")"
 
+/--
+The `(exp := n)` syntax for `linear_combination` says to take the goal to the `n`th power before
+subtracting the given combination of hypotheses.
+-/
 syntax expStx := atomic(" (" &"exp" " := ") withoutPosition(num) ")"
 
 /--
@@ -172,6 +176,10 @@ Note: The left and right sides of all the equalities should have the same
   * To get a subgoal in the case that it is not immediately provable, use
     `ring_nf` as the normalization tactic.
   * To avoid normalization entirely, use `skip` as the normalization tactic.
+* `linear_combination (exp := n) e` will take the goal to the `n`th power before subtracting the
+  combination `e`. In other words, if the goal is `t1 = t2`, `linear_combination (exp := n) e`
+  will change the goal to `(t1 - t2)^n = 0` before proceeding as above.
+  This feature is not supported for `linear_combination2`.
 * `linear_combination2 e` is the same as `linear_combination e` but it produces two
   subgoals instead of one: rather than proving that `(a - b) - (a' - b') = 0` where
   `a' = b'` is the linear combination from `e` and `a = b` is the goal,

From 74c822dff7356e5bfbbfdf1e1286fa59d442cdd0 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Tue, 17 Oct 2023 22:05:26 -0400
Subject: [PATCH 05/12] start on extending polyrith

---
 Mathlib/Tactic/Polyrith.lean | 14 ++++++++++----
 scripts/polyrith_sage.py     | 27 ++++++++++++++++-----------
 2 files changed, 26 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 4ee028d7c404a..39b58e7e89563 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -250,14 +250,20 @@ instance : FromJson Poly where
         mon := mon.mul' (.pow' (← fromJson? (← j.getArrVal? 0)) (← fromJson? (← j.getArrVal? 1)))
       pure mon
 
+/-- A schema for the data reported by the Sage calculation -/
+structure SageCoeffAndPower where
+  /-- The function call produces an array of polynomials
+  parallel to the input list of hypotheses. -/
+  coeffs : Array Poly
+  power  : ℕ
+  deriving FromJson, Repr
+
 /-- The result of a sage call in the success case. -/
 structure SageSuccess where
   /-- The script returns a string containing python script to be sent to the remote server,
   when the tracing option is set. -/
   trace : Option String := none
-  /-- The main result of the function call is an array of polynomials
-  parallel to the input list of hypotheses. -/
-  data : Option (Array Poly) := none
+  data : Option SageCoeffAndPower := none
   deriving FromJson, Repr
 
 /-- The result of a sage call in the failure case. -/
@@ -337,7 +343,7 @@ def polyrith (g : MVarId) (only : Bool) (hyps : Array Expr)
     match ← sageOutput (createSageArgs traceOnly α vars hyps' tgt) with
     | .ok { trace, data } =>
       if let some trace := trace then logInfo trace
-      if let some polys := data then
+      if let some {coeffs := polys, power := pow} := data then
         let vars ← liftM <| (← get).atoms.mapM delab
         let p ← Poly.sumM (polys.zip hyps') fun (p, src, _) => do
           let h := .hyp (← delab (match src with | .input i => hyps[i]! | .fvar h => .fvar h))
diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index f25beea928b36..96eddcbaa6aad 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -19,15 +19,19 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     """ Create a query to invoke Sage's `MPolynomial_libsingular.lift`. See
     https://github.com/sagemath/sage/blob/f8df80820dc7321dc9b18c9644c3b8315999670b/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx#L4472-L4518
     for a description of this method. """
-    var_list = ", ".join([f"var{i}" for i in range(n_vars)])
+    var_list = [f"var{i}" for i in range(n_vars)] + ['aux']
     query = f'''
-P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
-[{var_list}] = P.gens()
-gens = {eq_list}
+import json
+P = {type_str(type)}{var_list}
+[{", ".join(var_list)}] = P.gens()
 p = P({goal_type})
+gens = {eq_list} + [1 - p*aux]
 I = ideal(gens)
-coeffs = p.lift(I)
-print(serialize_polynomials(coeffs))
+coeffs = P(1).lift(I)
+power = max(cf.degree(aux) for cf in coeffs)
+coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]]
+js = {{'power': power, 'coeffs': [polynomial_to_string(c) for c in coeffs]}}
+print(json.dumps(js))
 '''
     return query
 
@@ -52,7 +56,7 @@ def evaluate_in_sage(query: str) -> str:
 def main():
     '''The system args contain the following:
     0 - the path to this python file
-    1 - a string containing "true" or "false" depending on whether polyrith was called with trace enabled
+    1 - a string containing "tt" or "ff" depending on whether polyrith was called with trace enabled
     2 - a string representing the base type of the target
     3 - the number of variables used
     4 - a list of the polynomial hypotheses/proof terms in terms of the variables
@@ -63,20 +67,21 @@ def main():
     { success: bool,
       data: Optional[list[str]],
       trace: Optional[str],
-      name: Optional[str],
-      value: Optional[str] }
+      error_name: Optional[str],
+      error_value: Optional[str] }
     ```
     '''
     command = create_query(sys.argv[2], int(sys.argv[3]), sys.argv[4], sys.argv[5])
     final_query = polynomial_formatting_functions + "\n" + command
-    if sys.argv[1] == 'true': # trace dry run enabled
+    if sys.argv[1] == 'tt': # trace dry run enabled
         output = dict(success=True, trace=command)
     else:
         try:
             output = dict(success=True, data=evaluate_in_sage(final_query))
         except EvaluationError as e:
-            output = dict(success=False, name=e.ename, value=e.evalue)
+            output = dict(success=False, error_name=e.ename, error_value=e.evalue)
     print(json.dumps(output))
 
+
 if __name__ == "__main__":
     main()

From 93445f90439c0088c95eac935563347706b41256 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 22:11:18 -0400
Subject: [PATCH 06/12] wip

---
 Mathlib/Tactic/Polyrith.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 39b58e7e89563..a64d19ac314c6 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -353,7 +353,8 @@ def polyrith (g : MVarId) (only : Bool) (hyps : Array Expr)
         let stx := (withRef (← getRef) <| p.toSyntax vars).run
         let tac ←
           if let .const 0 := p then `(tactic| linear_combination)
-          else `(tactic| linear_combination $stx:term)
+          else if pow = 1 then `(tactic| linear_combination $stx:term)
+          else `(tactic| linear_combination (exp := $(quote pow)) $stx:term)
         try
           guard (← Elab.runTactic g tac).1.isEmpty
         catch _ => throwError

From 8d7e896f627c1e0a7e7d73ea72d89e8a648dae8d Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Thu, 19 Oct 2023 23:27:36 -0400
Subject: [PATCH 07/12] complete and add tests

---
 scripts/polyrith_sage.py | 52 ++++++++++++++++++++++++++--------------
 test/polyrith.lean       | 20 ++++++++++++++++
 2 files changed, 54 insertions(+), 18 deletions(-)

diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index 96eddcbaa6aad..5567c36d6a97c 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -21,20 +21,31 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     for a description of this method. """
     var_list = [f"var{i}" for i in range(n_vars)] + ['aux']
     query = f'''
-import json
-P = {type_str(type)}{var_list}
-[{", ".join(var_list)}] = P.gens()
-p = P({goal_type})
-gens = {eq_list} + [1 - p*aux]
-I = ideal(gens)
-coeffs = P(1).lift(I)
-power = max(cf.degree(aux) for cf in coeffs)
-coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]]
-js = {{'power': power, 'coeffs': [polynomial_to_string(c) for c in coeffs]}}
-print(json.dumps(js))
+if {n_vars!r} != 0:
+    P = PolynomialRing({type_str(type)}, {var_list})
+    [{", ".join(var_list)}] = P.gens()
+    p = P({goal_type})
+    gens = {eq_list} + [1 - p*aux]
+    I = P.ideal(gens)
+    coeffs = P(1).lift(I)
+    power = max(cf.degree(aux) for cf in coeffs)
+    coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]]
+    print(str(power)+';'+serialize_polynomials(coeffs))
+else:
+    # workaround for a Sage shortcoming with `n_vars = 0`,
+    # `TypeError: no conversion of this ring to a Singular ring defined`
+    P = PolynomialRing({type_str(type)}, 'var', 1)
+    p = P({goal_type})
+    I = P.ideal({eq_list})
+    coeffs = p.lift(I)
+    print('1;'+serialize_polynomials(coeffs))
 '''
     return query
 
+def log(str):
+    with open('logfile.txt', 'w') as out:
+        out.write(str)
+
 class EvaluationError(Exception):
     def __init__(self, ename, evalue, message='Error in Sage communication'):
         self.ename = ename
@@ -42,12 +53,17 @@ def __init__(self, ename, evalue, message='Error in Sage communication'):
         self.message = message
         super().__init__(self.message)
 
+def parse_response(resp: str) -> str:
+    exp, data = resp.split(';', 1)
+    return dict(power=int(exp), coeffs=json.loads(data))
+
+
 def evaluate_in_sage(query: str) -> str:
     data = {'code': query}
     headers = {'content-type': 'application/x-www-form-urlencoded'}
     response = requests.post('https://sagecell.sagemath.org/service', data, headers=headers).json()
     if response['success']:
-        return json.loads(response.get('stdout'))
+        return parse_response(response.get('stdout'))
     elif 'execute_reply' in response and 'ename' in response['execute_reply'] and 'evalue' in response['execute_reply']:
         raise EvaluationError(response['execute_reply']['ename'], response['execute_reply']['evalue'])
     else:
@@ -56,7 +72,7 @@ def evaluate_in_sage(query: str) -> str:
 def main():
     '''The system args contain the following:
     0 - the path to this python file
-    1 - a string containing "tt" or "ff" depending on whether polyrith was called with trace enabled
+    1 - a string containing "true" or "false" depending on whether polyrith was called with trace enabled
     2 - a string representing the base type of the target
     3 - the number of variables used
     4 - a list of the polynomial hypotheses/proof terms in terms of the variables
@@ -67,21 +83,21 @@ def main():
     { success: bool,
       data: Optional[list[str]],
       trace: Optional[str],
-      error_name: Optional[str],
-      error_value: Optional[str] }
+      name: Optional[str],
+      value: Optional[str] }
     ```
     '''
     command = create_query(sys.argv[2], int(sys.argv[3]), sys.argv[4], sys.argv[5])
     final_query = polynomial_formatting_functions + "\n" + command
-    if sys.argv[1] == 'tt': # trace dry run enabled
+    log(final_query)
+    if sys.argv[1] == 'true': # trace dry run enabled
         output = dict(success=True, trace=command)
     else:
         try:
             output = dict(success=True, data=evaluate_in_sage(final_query))
         except EvaluationError as e:
-            output = dict(success=False, error_name=e.ename, error_value=e.evalue)
+            output = dict(success=False, name=e.ename, value=e.evalue)
     print(json.dumps(output))
 
-
 if __name__ == "__main__":
     main()
diff --git a/test/polyrith.lean b/test/polyrith.lean
index 5123abc612765..78457e74397e1 100644
--- a/test/polyrith.lean
+++ b/test/polyrith.lean
@@ -545,6 +545,26 @@ by polyrith
 --   polyrith,
 -- end
 
+/-
+
+### Examples with exponent
+
+-/
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := by
+  polyrith
+
+example (K : Type)
+    [Field K]
+    [CharZero K]
+    {x y z : K}
+    (h₂ : y ^ 3 + x * (3 * z ^ 2) = 0)
+    (h₁ : x ^ 3 + z * (3 * y ^ 2) = 0)
+    (h₀ : y * (3 * x ^ 2) + z ^ 3 = 0)
+    (h : x ^ 3 * y + y ^ 3 * z + z ^ 3 * x = 0) :
+    x = 0 := by
+  polyrith
+
 /-!
 ### With trace enabled
 Here, the tactic will trace the command that gets sent to sage,

From c30c0459948502979983f5c0f1c6b290a0c1df68 Mon Sep 17 00:00:00 2001
From: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Fri, 20 Oct 2023 09:01:59 -0400
Subject: [PATCH 08/12] Apply suggestions from code review

---
 Mathlib/Tactic/Polyrith.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index ffa73c5a2abf4..2b09841914df5 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -255,6 +255,8 @@ structure SageCoeffAndPower where
   /-- The function call produces an array of polynomials
   parallel to the input list of hypotheses. -/
   coeffs : Array Poly
+  /-- Sage produces an exponent (default 1) in the case where the hypothesess
+  sum to a power of the goal. -/
   power  : ℕ
   deriving FromJson, Repr
 
@@ -263,6 +265,8 @@ structure SageSuccess where
   /-- The script returns a string containing python script to be sent to the remote server,
   when the tracing option is set. -/
   trace : Option String := none
+  /-- The main result of the function call is an array of polynomials
+  parallel to the input list of hypotheses and an exponent for the goal. -/
   data : Option SageCoeffAndPower := none
   deriving FromJson, Repr
 

From bc33e63c4d7b8dcc306ef854198fe89134ae3a39 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Fri, 20 Oct 2023 11:41:41 -0400
Subject: [PATCH 09/12] docs

---
 Mathlib/Tactic/Polyrith.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 2b09841914df5..b02874c7dd5c1 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -33,6 +33,11 @@ It then calls a Python file that uses the SageMath API to compute the coefficien
 coefficients are then sent back to Lean, which parses them into pexprs. The information is then
 given to the `linear_combination` tactic, which completes the process by checking the certificate.
 
+In fact, `polyrith` uses Sage to test for membership in the *radical* of the ideal.
+This means it searches for a linear combination of hypotheses that add up to a *power* of the goal.
+When this power is not 1, it uses the `(exp := n)` feature of `linear_combination` to report the
+certificate.
+
 `polyrith` calls an external python script `scripts/polyrith_sage.py`. Because this is not a Lean
 file, changes to this script may not be noticed during Lean compilation if you have already
 generated olean files. If you are modifying this python script, you likely know what you're doing;

From d8873f0ca16f1323128687564ff7655ec08f2ce2 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 21 Oct 2023 17:32:27 -0400
Subject: [PATCH 10/12] chore: bump lean toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index a61d282854d89..183a307edb2d1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc3
+leanprover/lean4:v4.2.0-rc4

From bbcb66dc4b4b8eeea07f186f8f03fa1600a0a429 Mon Sep 17 00:00:00 2001
From: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Tue, 24 Oct 2023 12:30:33 -0400
Subject: [PATCH 11/12] remove debug code

---
 scripts/polyrith_sage.py | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index 5567c36d6a97c..5870456acdf04 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -42,10 +42,6 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
 '''
     return query
 
-def log(str):
-    with open('logfile.txt', 'w') as out:
-        out.write(str)
-
 class EvaluationError(Exception):
     def __init__(self, ename, evalue, message='Error in Sage communication'):
         self.ename = ename
@@ -89,7 +85,6 @@ def main():
     '''
     command = create_query(sys.argv[2], int(sys.argv[3]), sys.argv[4], sys.argv[5])
     final_query = polynomial_formatting_functions + "\n" + command
-    log(final_query)
     if sys.argv[1] == 'true': # trace dry run enabled
         output = dict(success=True, trace=command)
     else:

From 677d35e28e2b836ee41e068ae55857c51bbdcf2d Mon Sep 17 00:00:00 2001
From: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Fri, 3 Nov 2023 14:18:58 -0400
Subject: [PATCH 12/12] expand comment about workaround case

---
 scripts/polyrith_sage.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index 5870456acdf04..f9937c85ba2cd 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -34,6 +34,9 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
 else:
     # workaround for a Sage shortcoming with `n_vars = 0`,
     # `TypeError: no conversion of this ring to a Singular ring defined`
+    # In this case, there is no need to look for membership in the *radical*;
+    # we just check for membership in the ideal, and return exponent 1 
+    # if coefficients are found.
     P = PolynomialRing({type_str(type)}, 'var', 1)
     p = P({goal_type})
     I = P.ideal({eq_list})