From c94497506f6f35043c91a7403bc246d30f89f62c Mon Sep 17 00:00:00 2001
From: Elias Judin <ejudin@gmail.com>
Date: Tue, 3 Mar 2026 12:10:59 +0200
Subject: [PATCH] Implement CMvPolynomial CommRing via transfer lemmas

Move transfer lemmas and ring-instance machinery into CMvPolynomial and make MvPolyEquiv reuse those declarations to break the circular dependency and close the #55 CommRing gap.

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 CompPoly/Multivariate/CMvPolynomial.lean | 382 +++++++++++++++++++++--
 CompPoly/Multivariate/MvPolyEquiv.lean   | 295 +----------------
 2 files changed, 352 insertions(+), 325 deletions(-)

diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean
index 7b7e14a..e495064 100644
--- a/CompPoly/Multivariate/CMvPolynomial.lean
+++ b/CompPoly/Multivariate/CMvPolynomial.lean
@@ -7,6 +7,8 @@ import CompPoly.Multivariate.Lawful
 import CompPoly.Univariate.Basic
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
+import Mathlib.Algebra.MvPolynomial.Basic
+import Batteries.Data.Vector.Lemmas
 
 /-!
 # Computable multivariate polynomials
@@ -259,39 +261,357 @@ def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 
 -- `renameEquiv` is defined in `CompPoly.Multivariate.Rename`
 
-/-- `CMvPolynomial n R` forms a commutative ring when `R` is a commutative ring.
+end CMvPolynomial
 
-  Extends the `CommSemiring` structure with subtraction.
+/-! ### Ring instances via transfer from `MvPolynomial`
+
+The ring structure on `CMvPolynomial n R` is established by defining an injection
+`fromCMvPolynomial : CMvPolynomial n R → MvPolynomial (Fin n) R` and transferring
+the ring axioms from `MvPolynomial`. -/
+
+section RingInstances
+
+open CMvPolynomial
+
+variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
+
+/-- Map a `CMvPolynomial` to the corresponding `MvPolynomial` for algebraic transfer. -/
+def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R :=
+  let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp
+  let toFun (f : Fin n →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0
+  let mem_support_fun {a : Fin n →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind
+  Finsupp.mk support.toFinset toFun (by simp [mem_support_fun])
+
+omit [BEq R] [LawfulBEq R] in
+lemma coeff_eq {m} (a : CMvPolynomial n R) :
+    MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := rfl
+
+@[aesop simp]
+lemma eq_iff_fromCMvPolynomial {u v : CMvPolynomial n R} :
+    u = v ↔ fromCMvPolynomial u = fromCMvPolynomial v := by
+  constructor
+  · rintro rfl; rfl
+  · intro h
+    ext m
+    have : MvPolynomial.coeff (CMvMonomial.toFinsupp m) (fromCMvPolynomial u) =
+           MvPolynomial.coeff (CMvMonomial.toFinsupp m) (fromCMvPolynomial v) := by rw [h]
+    simp only [coeff_eq, CMvMonomial.ofFinsupp_toFinsupp] at this
+    exact this
+
+lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _) := by
+  intros a b h
+  exact eq_iff_fromCMvPolynomial.mpr h
+
+@[simp]
+lemma map_add (a b : CMvPolynomial n R) :
+    fromCMvPolynomial (a + b) = fromCMvPolynomial a + fromCMvPolynomial b := by
+  ext m
+  rw [MvPolynomial.coeff_add, coeff_eq, coeff_eq, coeff_eq]
+  unfold CMvPolynomial.coeff
+  unfold_projs
+  unfold CPoly.Lawful.add
+  simp only [ExtTreeMap.get?_eq_getElem?, Unlawful.zero_eq_zero]
+  unfold_projs
+  unfold Unlawful.add Lawful.fromUnlawful
+  simp only [ExtTreeMap.get?_eq_getElem?, Unlawful.zero_eq_zero]
+  erw [Unlawful.filter_get]
+  by_cases h : (CMvMonomial.ofFinsupp m) ∈ a.1 <;> by_cases h' : (CMvMonomial.ofFinsupp m) ∈ b.1
+  · erw [ExtTreeMap.mergeWith_of_mem_mem h h', Option.getD_some]
+    have h₁ : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) =
+      (a.1)[CMvMonomial.ofFinsupp m] := by simp [h]
+    have h₂ : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) =
+      (b.1)[CMvMonomial.ofFinsupp m] := by simp [h']
+    erw [h₁, h₂]
+    rfl
+  · erw [ExtTreeMap.mergeWith_of_mem_left h h']
+    have : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
+      simp [h']
+    erw [this]
+    have {x : R} : x + 0 = x := by simp
+    specialize @this ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0)
+    unfold_projs at this
+    erw [this]
+    rfl
+  · erw [ExtTreeMap.mergeWith_of_mem_right h h']
+    have : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
+      simp [h]
+    erw [this]
+    have {x : R} : 0 + x = x := by simp
+    specialize @this ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0)
+    unfold_projs at this
+    erw [this]
+    rfl
+  · erw [ExtTreeMap.mergeWith_of_not_mem h h']
+    have h₁ : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
+      simp [h]
+    have h₂ : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
+      simp [h']
+    erw [h₁, h₂, Option.getD_none]
+    have : 0 + 0 = (0 : R) := by simp
+    unfold_projs at this
+    erw [this]
+    rfl
+
+@[simp]
+lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial n R) = 0 := by
+  ext m
+  rw [MvPolynomial.coeff_zero]
+  unfold fromCMvPolynomial
+  simp only
+    [ Lawful.mem_iff_cast,
+      Lawful.not_mem_zero,
+      not_false_eq_true,
+      getElem?_neg, Option.getD_none
+    ]
+  rfl
 
-  TODO: Requires `CommSemiring` instance (defined in MvPolyEquiv.lean).
-  TODO: Verify Neg/Sub operations exist in Lawful.lean.
-  Note: Cannot import MvPolyEquiv.lean due to circular dependency, so all fields are `sorry`.
--/
-instance {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] :
-    CommRing (CMvPolynomial n R) where
-  add_assoc := sorry
-  zero_add := sorry
-  add_zero := sorry
-  nsmul := sorry
-  nsmul_zero := sorry
-  nsmul_succ := sorry
-  add_comm := sorry
-  left_distrib := sorry
-  right_distrib := sorry
-  zero_mul := sorry
-  mul_zero := sorry
-  mul_assoc := sorry
-  one_mul := sorry
-  mul_one := sorry
-  npow := sorry
-  npow_zero := sorry
-  npow_succ := sorry
-  zsmul := sorry
-  zsmul_zero' := sorry
-  zsmul_succ' := sorry
-  zsmul_neg' := sorry
-  neg_add_cancel := sorry
-  mul_comm := sorry
+instance : TransCmp (fun x y ↦ compareOfLessAndEq (α := ℕ) x y) where
+  eq_swap {a b} := by apply compareOfLessAndEq_eq_swap <;> omega
+  isLE_trans {a b c} h₁ h₂ := by rw [isLE_compareOfLessAndEq] at * <;> omega
+
+instance {n : ℕ} : TransCmp (α := CMvMonomial n)
+    (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y) :=
+  inferInstanceAs (TransCmp (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y))
+
+@[simp]
+lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 := by
+  ext m
+  have : MvPolynomial.coeff m 1 = if m = 0 then 1 else (0 : R) := by
+    unfold MvPolynomial.coeff
+    unfold_projs
+    simp only [Nat.zero_eq, Unlawful.zero_eq_zero]
+    split_ifs with h <;>
+      unfold AddMonoidAlgebra.single Finsupp.toFun Finsupp.single <;>
+        simp [h]
+  rw [this]
+  unfold fromCMvPolynomial MvPolynomial.coeff
+  simp only [Lawful.getElem?_eq_val_getElem?, Finsupp.coe_mk]
+  unfold_projs
+  unfold Lawful.C Unlawful.C MonoR.C
+  simp only [Nat.cast_one]
+
+  have triv_lem : (1 : R) = 0 → ∀ x y : R, x = y := by
+    intros h
+    have (x : R) : x = 0 := by
+      have : x * 1 = x * 0 := by
+        rw [h]
+      simp only [mul_one, mul_zero] at this
+      exact this
+    intros x y; rw [this x, this y]
+
+  split_ifs with g g' g'
+  · rw [Nat.cast_one] at g; apply triv_lem g
+  · rw [Nat.cast_one] at g; apply triv_lem g
+  · have finsupp_m_eq_one : CMvMonomial.ofFinsupp m = CMvMonomial.zero := by
+      rw [g']
+      unfold CMvMonomial.ofFinsupp CMvMonomial.zero
+      ext i h
+      simp only [Nat.zero_eq, Finsupp.coe_mk]
+      grind
+    rw [finsupp_m_eq_one]
+    have one_one_get₁ :
+      ({(CMvMonomial.zero, 1)} : Unlawful n R)[(@CMvMonomial.zero n)]?.getD 0 = One.one := by
+      unfold_projs; simp only [ExtTreeMap.empty_eq_emptyc, ExtTreeMap.get?_eq_getElem?,
+        ExtTreeMap.getElem?_insert_self, Unlawful.zero_eq_zero, Option.getD_some]
+    convert one_one_get₁
+  · have : CMvMonomial.ofFinsupp m ≠ CMvMonomial.zero := by
+      unfold CMvMonomial.ofFinsupp CMvMonomial.zero
+      intros h
+      have {i} : (Vector.ofFn m).get i = (Vector.replicate n 0).get i := by
+        rw [h]
+      apply g'
+      ext i
+      simp only [Finsupp.coe_mk]
+      simp only [Vector.get_ofFn, Vector.get_replicate] at this
+      exact this
+    rw [ExtTreeMap.get?_eq_getElem?, getElem?_neg]
+    simp only [Unlawful.zero_eq_zero, Option.getD_none]
+    unfold Unlawful.ofList
+    simp only [ExtTreeMap.ofList_singleton, ExtTreeMap.mem_insert, Std.compare_eq_iff_eq,
+      ExtTreeMap.not_mem_empty, or_false]
+    tauto
+
+attribute [local grind=] Unlawful.add Lawful.add Unlawful.mul Lawful.mul
+
+instance instAddCommSemigroup {n : ℕ} : AddCommSemigroup (CPoly.CMvPolynomial n R) where
+  add_assoc := by aesop (add safe apply add_assoc)
+  add_comm := by grind
+
+instance instAddMonoid {n : ℕ} : AddMonoid (CPoly.CMvPolynomial n R) where
+  zero_add _ := by aesop
+  add_zero _ := by aesop
+  nsmul n p := (List.replicate n p).sum
+  nsmul_succ {m x} := by grind
+
+instance instAddCommMonoid {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where
+  toAddMonoid := inferInstance
+  add_comm := by grind
+
+omit [BEq R] [LawfulBEq R] in
+lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β]
+    {t : Unlawful n R}
+  {f : CMvMonomial n → R → β} :
+  t.toList.map (fun term => f term.1 term.2) =
+    t.monomials.map (fun m => f m (t.coeff m)) := by
+  unfold Unlawful.monomials Unlawful.coeff
+  rw [←ExtTreeMap.map_fst_toList_eq_keys]
+  rw [List.map_congr_left, List.map_map]
+  grind
+
+omit [BEq R] [LawfulBEq R] in
+lemma foldl_eq_sum {β : Type} [AddCommMonoid β]
+    {t : CMvPolynomial n R}
+    {f : CMvMonomial n → R → β} :
+    ExtTreeMap.foldl (fun x m c => (f m c) + x) 0 t.1 =
+      Finsupp.sum (fromCMvPolynomial t) (f ∘ CMvMonomial.ofFinsupp) := by
+  unfold Finsupp.sum Finset.sum
+  simp only [Function.comp_apply, add_comm]
+  rw [ExtTreeMap.foldl_eq_foldl_toList]
+  rw [←List.foldl_map (g := fun x y ↦ x + y), ←List.sum_eq_foldl]
+  rw [toList_pairs_monomial_coeff]
+  conv => rhs; arg 1; arg 1; ext x; arg 2; rw [←MvPolynomial.coeff, coeff_eq]
+  congr 1
+  have monomials_dedup_self : (Lawful.monomials t).dedup = Lawful.monomials t := by
+    unfold Lawful.monomials
+    simp only [List.dedup_eq_self]
+    grind [ExtTreeMap.distinct_keys_toList]
+  rw [List.dedup_map_of_injective CMvMonomial.injective_toFinsupp]
+  rw [monomials_dedup_self]
+  aesop
+
+lemma coeff_sum [AddCommMonoid α]
+    (s : Finset α)
+    (f : α → CMvPolynomial n R)
+    (m : CMvMonomial n) :
+    CMvPolynomial.coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, CMvPolynomial.coeff m (f x) := by
+  rw [←Finset.sum_map_toList s, ←Finset.sum_map_toList s]
+  induction' s.toList with h t ih
+  · grind
+  · simp [CMvPolynomial.coeff_add]
+    congr
+
+lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial
+    {f : (Fin n →₀ ℕ) → R → Lawful n R }
+    {a : CMvPolynomial n R} :
+    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) f) =
+      Finsupp.sum (fromCMvPolynomial a) (fun m c ↦ fromCMvPolynomial (f m c)) := by
+  unfold Finsupp.sum; ext
+  simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
+
+@[simp]
+lemma map_mul (a b : CMvPolynomial n R) :
+    fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b := by
+  dsimp only [HMul.hMul, Mul.mul, Lawful.mul, Unlawful.mul]
+  simp only [CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful]
+  unfold MonoidAlgebra.mul'
+  rw [foldl_eq_sum]; simp_rw [foldl_eq_sum]
+  let F₀ (p q) : CMvMonomial n → R → Lawful n R :=
+    fun p_1 q_1 ↦ Lawful.fromUnlawful {(p + p_1 , q * q_1)}
+  set F₁ : (Fin n →₀ ℕ) → R → Lawful n R :=
+    (fun p q ↦ Finsupp.sum (fromCMvPolynomial b) (F₀ p q ∘ CMvMonomial.ofFinsupp))
+      ∘ CMvMonomial.ofFinsupp with eqF₁
+  let F₂ a₁ b₁ :
+    Multiplicative (Fin n →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (Fin n →₀ ℕ)) :=
+    fun a₂ b₂ ↦ MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
+  set F₃ : Multiplicative (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R :=
+    fun a₁ b₁ ↦ Finsupp.sum (fromCMvPolynomial b) (F₂ a₁ b₁) with eqF₃
+  have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (Fin n →₀ ℕ)} {c₁ : R} :
+      fromCMvPolynomial (F₁ m₁ c₁) = F₃ m₁ c₁ := by
+    dsimp only [Function.comp_apply, F₁, F₀, F₃, F₂]
+    rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
+    simp only [Function.comp_apply]
+    congr
+    ext (m₂ : Multiplicative _) c₂ m
+    rw [coeff_eq]
+    unfold CMvPolynomial.coeff Lawful.fromUnlawful
+    erw [Unlawful.filter_get, ←CMvMonomial.map_mul, ExtTreeMap.singleton_eq_insert]
+    erw [ExtTreeMap.getElem?_insert]
+    by_cases m_in : m = m₁ * m₂
+    · rw [←m_in]
+      simp only [compare_self]
+      unfold MvPolynomial.coeff MonoidAlgebra.single
+      simp only [m_in, Finsupp.single_eq_same]
+      rfl
+    · simp only
+        [ Std.compare_eq_iff_eq,
+          ExtTreeMap.not_mem_empty,
+          not_false_eq_true,
+          getElem?_neg
+        ]
+      unfold MvPolynomial.coeff MonoidAlgebra.single
+      rw [Finsupp.single_eq_of_ne (by symm; grind)]
+      split
+      next h contra =>
+        exfalso; apply m_in; symm
+        apply CMvMonomial.injective_ofFinsupp contra
+      next h => simp_all only [Option.getD_none]
+  have : F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) := by
+    ext x
+    rw [fromCMvPolynomial_F₁_eq_F₃]
+  rw [this]
+  rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
+  rfl
+
+instance instMonoidWithZero {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where
+  zero_mul := by aesop
+  mul_zero := by aesop
+  mul_assoc := by aesop (add safe apply _root_.mul_assoc)
+  one_mul := by aesop
+  mul_one := by aesop
+
+instance instSemiring {n : ℕ} : Semiring (CPoly.CMvPolynomial n R) where
+  left_distrib {p q r} := by
+    simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add]
+    apply mul_add
+  right_distrib {p q r} := by
+    simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add]
+    apply add_mul
+
+instance instCommSemiring {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where
+  natCast_zero := by grind
+  natCast_succ := by intro n; simp
+  npow_zero := by intro x; simp [npowRecAuto, npowRec]
+  npow_succ := by intro n x; simp [npowRecAuto, npowRec]
+  mul_comm := by aesop (add safe apply _root_.mul_comm)
+
+end RingInstances
+
+section CommRingInstance
+
+open CMvPolynomial
+
+variable {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R]
+
+@[simp]
+lemma map_neg (a : CMvPolynomial n R) :
+    fromCMvPolynomial (-a) = -fromCMvPolynomial a := by
+  ext m
+  rw [coeff_eq]
+  simp only [MvPolynomial.coeff_neg, coeff_eq]
+  unfold CMvPolynomial.coeff
+  show (Lawful.fromUnlawful (a.1.map fun _ v ↦ -v)).1[CMvMonomial.ofFinsupp m]?.getD 0 =
+       -(a.1[CMvMonomial.ofFinsupp m]?.getD 0)
+  change (Lawful.fromUnlawful (a.1.map fun _ v ↦ -v)).1[CMvMonomial.ofFinsupp m]?.getD 0 =
+       -(a.1[CMvMonomial.ofFinsupp m]?.getD 0)
+  conv_lhs => simp only [Lawful.fromUnlawful]
+  erw [Unlawful.filter_get (a := (a.1.map fun _ v ↦ -v))]
+  erw [ExtTreeMap.getElem?_map]
+  cases a.1[CMvMonomial.ofFinsupp m]? with
+  | none => simp
+  | some v => simp
+
+/-- `CMvPolynomial n R` forms a commutative ring when `R` is a commutative ring. -/
+instance instCommRing {n : ℕ} : CommRing (CMvPolynomial n R) where
+  __ := instCommSemiring (R := R)
+  neg_add_cancel a := by
+    rw [eq_iff_fromCMvPolynomial]
+    simp [map_add, map_neg, map_zero]
+  zsmul := zsmulRec
+  mul_comm := mul_comm
+
+end CommRingInstance
+
+namespace CMvPolynomial
 
 /-- Convert sum representation to iterative form.
 
diff --git a/CompPoly/Multivariate/MvPolyEquiv.lean b/CompPoly/Multivariate/MvPolyEquiv.lean
index 4eb6e43..04bccb4 100644
--- a/CompPoly/Multivariate/MvPolyEquiv.lean
+++ b/CompPoly/Multivariate/MvPolyEquiv.lean
@@ -28,12 +28,6 @@ section
 
 variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 
-def fromCMvPolynomial  (p : CMvPolynomial n R) : MvPolynomial (Fin n) R :=
-  let support : List (Fin n →₀ ℕ) := p.monomials.map CMvMonomial.toFinsupp
-  let toFun (f : Fin n →₀ ℕ) : R := p[CMvMonomial.ofFinsupp f]?.getD 0
-  let mem_support_fun {a : Fin n →₀ ℕ} : a ∈ support ↔ toFun a ≠ 0 := by grind
-  Finsupp.mk support.toFinset toFun (by simp [mem_support_fun])
-
 noncomputable def toCMvPolynomial (p : MvPolynomial (Fin n) R) : CMvPolynomial n R :=
   let ⟨s, f, _⟩ := p
   let unlawful := .ofList <| s.toList.map fun m ↦ (CMvMonomial.ofFinsupp m, f m)
@@ -104,150 +98,6 @@ theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial (Fin n) R} :
   · have : ∀ x ∈ s, CMvMonomial.ofFinsupp x ≠ CMvMonomial.ofFinsupp m := by aesop
     grind
 
-lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _) := by
-  rw [Function.injective_iff_hasLeftInverse]
-  exists toCMvPolynomial
-  apply toCMvPolynomial_fromCMvPolynomial
-
-omit [BEq R] [LawfulBEq R] in
-lemma coeff_eq {m} (a : CMvPolynomial n R) :
-    MvPolynomial.coeff m (fromCMvPolynomial a) = a.coeff (CMvMonomial.ofFinsupp m) := rfl
-
-@[aesop simp]
-lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial n R} :
-    u = v ↔ fromCMvPolynomial u = fromCMvPolynomial v := by
-  have := fromCMvPolynomial_injective (n := n) (R := R)
-  aesop
-
-@[simp]
-lemma map_add (a b : CMvPolynomial n R) :
-    fromCMvPolynomial (a + b) = fromCMvPolynomial a + fromCMvPolynomial b := by
-  ext m
-  rw [MvPolynomial.coeff_add, coeff_eq, coeff_eq, coeff_eq]
-  unfold CMvPolynomial.coeff
-  unfold_projs
-  unfold CPoly.Lawful.add
-  simp only [ExtTreeMap.get?_eq_getElem?, Unlawful.zero_eq_zero]
-  unfold_projs
-  unfold Unlawful.add Lawful.fromUnlawful
-  simp only [ExtTreeMap.get?_eq_getElem?, Unlawful.zero_eq_zero]
-  erw [Unlawful.filter_get]
-  by_cases h : (CMvMonomial.ofFinsupp m) ∈ a.1 <;> by_cases h' : (CMvMonomial.ofFinsupp m) ∈ b.1
-  · erw [ExtTreeMap.mergeWith_of_mem_mem h h', Option.getD_some]
-    have h₁ : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) =
-      (a.1)[CMvMonomial.ofFinsupp m] := by simp [h]
-    have h₂ : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) =
-      (b.1)[CMvMonomial.ofFinsupp m] := by simp [h']
-    erw [h₁, h₂]
-    rfl
-  · erw [ExtTreeMap.mergeWith_of_mem_left h h']
-    have : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
-      simp [h']
-    erw [this]
-    have {x : R} : x + 0 = x := by simp
-    specialize @this ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0)
-    unfold_projs at this
-    erw [this]
-    rfl
-  · erw [ExtTreeMap.mergeWith_of_mem_right h h']
-    have : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
-      simp [h]
-    erw [this]
-    have {x : R} : 0 + x = x := by simp
-    specialize @this ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0)
-    unfold_projs at this
-    erw [this]
-    rfl
-  · erw [ExtTreeMap.mergeWith_of_not_mem h h']
-    have h₁ : ((a.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
-      simp [h]
-    have h₂ : ((b.1)[CMvMonomial.ofFinsupp m]?.getD 0) = 0 := by
-      simp [h']
-    erw [h₁, h₂, Option.getD_none]
-    have : 0 + 0 = (0 : R) := by simp
-    unfold_projs at this
-    erw [this]
-    rfl
-
-@[simp]
-lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial n R) = 0 := by
-  ext m
-  rw [MvPolynomial.coeff_zero]
-  unfold fromCMvPolynomial
-  simp only
-    [ Lawful.mem_iff_cast,
-      Lawful.not_mem_zero,
-      not_false_eq_true,
-      getElem?_neg, Option.getD_none
-    ]
-  rfl
-
-instance : TransCmp (fun x y ↦ compareOfLessAndEq (α := ℕ) x y) where
-  eq_swap {a b} := by apply compareOfLessAndEq_eq_swap <;> omega
-  isLE_trans {a b c} h₁ h₂ := by rw [isLE_compareOfLessAndEq] at * <;> omega
-
-instance {n : ℕ} : TransCmp (α := CMvMonomial n)
-    (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y) :=
-  inferInstanceAs (TransCmp (Vector.compareLex (n := n) fun x y => compareOfLessAndEq (α := ℕ) x y))
-
-@[simp]
-lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 := by
-  ext m
-  have : MvPolynomial.coeff m 1 = if m = 0 then 1 else (0 : R) := by
-    unfold MvPolynomial.coeff
-    unfold_projs
-    simp only [Nat.zero_eq, Unlawful.zero_eq_zero]
-    split_ifs with h <;>
-      unfold AddMonoidAlgebra.single Finsupp.toFun Finsupp.single <;>
-        simp [h]
-  rw [this]
-  unfold fromCMvPolynomial MvPolynomial.coeff
-  simp only [Lawful.getElem?_eq_val_getElem?, Finsupp.coe_mk]
-  unfold_projs
-  unfold Lawful.C Unlawful.C MonoR.C
-  simp only [Nat.cast_one]
-
-  have triv_lem : (1 : R) = 0 → ∀ x y : R, x = y := by
-    intros h
-    have (x : R) : x = 0 := by
-      have : x * 1 = x * 0 := by
-        rw [h]
-      simp only [mul_one, mul_zero] at this
-      exact this
-    intros x y; rw [this x, this y]
-
-  split_ifs with g g' g'
-  · rw [Nat.cast_one] at g; apply triv_lem g
-  · rw [Nat.cast_one] at g; apply triv_lem g
-  · have finsupp_m_eq_one : CMvMonomial.ofFinsupp m = CMvMonomial.zero := by
-      rw [g']
-      unfold CMvMonomial.ofFinsupp CMvMonomial.zero
-      ext i h
-      simp only [Nat.zero_eq, Finsupp.coe_mk]
-      grind
-    rw [finsupp_m_eq_one]
-    have one_one_get₁ :
-      ({(CMvMonomial.zero, 1)} : Unlawful n R)[(@CMvMonomial.zero n)]?.getD 0 = One.one := by
-      unfold_projs; simp only [ExtTreeMap.empty_eq_emptyc, ExtTreeMap.get?_eq_getElem?,
-        ExtTreeMap.getElem?_insert_self, Unlawful.zero_eq_zero, Option.getD_some]
-    convert one_one_get₁
-  · have : CMvMonomial.ofFinsupp m ≠ CMvMonomial.zero := by
-      unfold CMvMonomial.ofFinsupp CMvMonomial.zero
-      intros h
-      have {i} : (Vector.ofFn m).get i = (Vector.replicate n 0).get i := by
-        rw [h]
-      apply g'
-      ext i
-      simp only [Finsupp.coe_mk]
-      simp only [Vector.get_ofFn, Vector.get_replicate] at this
-      exact this
-    rw [ExtTreeMap.get?_eq_getElem?, getElem?_neg]
-    simp only [Unlawful.zero_eq_zero, Option.getD_none]
-    unfold Unlawful.ofList
-    simp only [ExtTreeMap.ofList_singleton, ExtTreeMap.mem_insert, Std.compare_eq_iff_eq,
-      ExtTreeMap.not_mem_empty, or_false]
-    tauto
-
 noncomputable def polyEquiv :
     Equiv (CMvPolynomial n R) (MvPolynomial (Fin n) R) where
   toFun := fromCMvPolynomial
@@ -255,149 +105,6 @@ noncomputable def polyEquiv :
   left_inv := fun _ ↦ toCMvPolynomial_fromCMvPolynomial
   right_inv := fun _ ↦ fromCMvPolynomial_toCMvPolynomial
 
-attribute [local grind=] Unlawful.add Lawful.add Unlawful.mul Lawful.mul
-
-instance {n : ℕ} : AddCommSemigroup (CPoly.CMvPolynomial n R) where
-  add_assoc := by aesop (add safe apply add_assoc)
-  add_comm := by grind
-
-instance {n : ℕ} : AddMonoid (CPoly.CMvPolynomial n R) where
-  zero_add _ := by aesop
-  add_zero _ := by aesop
-  nsmul n p := (List.replicate n p).sum
-  nsmul_succ {m x} := by grind
-
-instance {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where
-  toAddMonoid := inferInstance
-  add_comm := by grind
-
-omit [BEq R] [LawfulBEq R] in
-lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β]
-    {t : Unlawful n R}
-  {f : CMvMonomial n → R → β} :
-  t.toList.map (fun term => f term.1 term.2) =
-    t.monomials.map (fun m => f m (t.coeff m)) := by
-  unfold Unlawful.monomials Unlawful.coeff
-  rw [←ExtTreeMap.map_fst_toList_eq_keys]
-  rw [List.map_congr_left, List.map_map]
-  grind
-
-omit [BEq R] [LawfulBEq R] in
-lemma foldl_eq_sum {β : Type} [AddCommMonoid β]
-    {t : CMvPolynomial n R}
-    {f : CMvMonomial n → R → β} :
-    ExtTreeMap.foldl (fun x m c => (f m c) + x) 0 t.1 =
-      Finsupp.sum (fromCMvPolynomial t) (f ∘ CMvMonomial.ofFinsupp) := by
-  unfold Finsupp.sum Finset.sum
-  simp only [Function.comp_apply, add_comm]
-  rw [ExtTreeMap.foldl_eq_foldl_toList]
-  rw [←List.foldl_map (g := fun x y ↦ x + y), ←List.sum_eq_foldl]
-  rw [toList_pairs_monomial_coeff]
-  conv => rhs; arg 1; arg 1; ext x; arg 2; rw [←MvPolynomial.coeff, coeff_eq]
-  congr 1
-  have monomials_dedup_self : (Lawful.monomials t).dedup = Lawful.monomials t := by
-    unfold Lawful.monomials
-    simp only [List.dedup_eq_self]
-    grind [ExtTreeMap.distinct_keys_toList]
-  rw [List.dedup_map_of_injective CMvMonomial.injective_toFinsupp]
-  rw [monomials_dedup_self]
-  aesop
-
-lemma coeff_sum [AddCommMonoid α]
-    (s : Finset α)
-    (f : α → CMvPolynomial n R)
-    (m : CMvMonomial n) :
-    coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x) := by
-  rw [←Finset.sum_map_toList s, ←Finset.sum_map_toList s]
-  induction' s.toList with h t ih
-  · grind
-  · simp [coeff_add]
-    congr
-
-lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial
-    {f : (Fin n →₀ ℕ) → R → Lawful n R }
-    {a : CMvPolynomial n R} :
-    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) f) =
-      Finsupp.sum (fromCMvPolynomial a) (fun m c ↦ fromCMvPolynomial (f m c)) := by
-  unfold Finsupp.sum; ext
-  simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
-
-@[simp]
-lemma map_mul (a b : CMvPolynomial n R) :
-    fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b := by
-  dsimp only [HMul.hMul, Mul.mul, Lawful.mul, Unlawful.mul]
-  simp only [CMvPolynomial.fromUnlawful_fold_eq_fold_fromUnlawful]
-  unfold MonoidAlgebra.mul'
-  rw [foldl_eq_sum]; simp_rw [foldl_eq_sum]
-  let F₀ (p q) : CMvMonomial n → R → Lawful n R :=
-    fun p_1 q_1 ↦ Lawful.fromUnlawful {(p + p_1 , q * q_1)}
-  set F₁ : (Fin n →₀ ℕ) → R → Lawful n R :=
-    (fun p q ↦ Finsupp.sum (fromCMvPolynomial b) (F₀ p q ∘ CMvMonomial.ofFinsupp))
-      ∘ CMvMonomial.ofFinsupp with eqF₁
-  let F₂ a₁ b₁ :
-    Multiplicative (Fin n →₀ ℕ) → R → MonoidAlgebra R (Multiplicative (Fin n →₀ ℕ)) :=
-    fun a₂ b₂ ↦ MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
-  set F₃ : Multiplicative (Fin n →₀ ℕ) → R → MvPolynomial (Fin n) R :=
-    fun a₁ b₁ ↦ Finsupp.sum (fromCMvPolynomial b) (F₂ a₁ b₁) with eqF₃
-  have fromCMvPolynomial_F₁_eq_F₃ {m₁ : Multiplicative (Fin n →₀ ℕ)} {c₁ : R} :
-      fromCMvPolynomial (F₁ m₁ c₁) = F₃ m₁ c₁ := by
-    dsimp only [Function.comp_apply, F₁, F₀, F₃, F₂]
-    rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
-    simp only [Function.comp_apply]
-    congr
-    ext (m₂ : Multiplicative _) c₂ m
-    rw [coeff_eq]
-    unfold coeff Lawful.fromUnlawful
-    erw [Unlawful.filter_get, ←CMvMonomial.map_mul, ExtTreeMap.singleton_eq_insert]
-    erw [ExtTreeMap.getElem?_insert]
-    by_cases m_in : m = m₁ * m₂
-    · rw [←m_in]
-      simp only [compare_self]
-      unfold MvPolynomial.coeff MonoidAlgebra.single
-      simp only [m_in, Finsupp.single_eq_same]
-      rfl
-    · simp only
-        [ Std.compare_eq_iff_eq,
-          ExtTreeMap.not_mem_empty,
-          not_false_eq_true,
-          getElem?_neg
-        ]
-      unfold MvPolynomial.coeff MonoidAlgebra.single
-      rw [Finsupp.single_eq_of_ne (by symm; grind)]
-      split
-      next h contra =>
-        exfalso; apply m_in; symm
-        apply CMvMonomial.injective_ofFinsupp contra
-      next h => simp_all only [Option.getD_none]
-  have : F₃ = fun σ x ↦ fromCMvPolynomial (F₁ σ x) := by
-    ext x
-    rw [fromCMvPolynomial_F₁_eq_F₃]
-  rw [this]
-  rw [fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial]
-  rfl
-
-instance {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where
-  zero_mul := by aesop
-  mul_zero := by aesop
-  mul_assoc := by aesop (add safe apply _root_.mul_assoc)
-  one_mul := by aesop
-  mul_one := by aesop
-
-instance {n : ℕ} : Semiring (CPoly.CMvPolynomial n R) where
-  left_distrib {p q r} := by
-    simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add]
-    apply mul_add
-  right_distrib {p q r} := by
-    simp_all only [eq_iff_fromCMvPolynomial, map_mul, map_add]
-    apply add_mul
-
-instance {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where
-  natCast_zero := by grind
-  natCast_succ := by intro n; simp
-  npow_zero := by intro x; simp [npowRecAuto, npowRec]
-  npow_succ := by intro n x; simp [npowRecAuto, npowRec]
-  mul_comm := by aesop (add safe apply _root_.mul_comm)
-
 noncomputable def polyRingEquiv :
   RingEquiv (CPoly.CMvPolynomial n R) (MvPolynomial (Fin n) R) where
   toEquiv := CPoly.polyEquiv
@@ -446,7 +153,7 @@ lemma degreeOf_equiv {S : Type} {p : CMvPolynomial n R} [CommSemiring S] :
   unfold MvPolynomial.degreeOf MvPolynomial.degrees
   unfold MvPolynomial.support fromCMvPolynomial
   simp only
-  unfold degreeOf
+  unfold CMvPolynomial.degreeOf
   congr
   unfold instDecidableEqFin Classical.decEq inferInstance
   unfold Classical.propDecidable