chore: merge Lean 4.30 version bump into gs-univariate-smooth

CompPoly.lean

@@ -99,6 +99,7 @@ import CompPoly.Univariate.BatchEval.Correctness
 import CompPoly.Univariate.BatchEval.Naive
 import CompPoly.Univariate.BatchEval.SubproductTree
 import CompPoly.Univariate.CMvEquiv
+import CompPoly.Univariate.Context
 import CompPoly.Univariate.Deriv
 import CompPoly.Univariate.DivisionCorrectness
 import CompPoly.Univariate.EuclideanAlgorithm
@@ -107,6 +108,7 @@ import CompPoly.Univariate.Linear
 import CompPoly.Univariate.ManyEval
 import CompPoly.Univariate.ManyEval.Basic
 import CompPoly.Univariate.ManyEval.Correctness
+import CompPoly.Univariate.Modular
 import CompPoly.Univariate.NTT.BabyBear
 import CompPoly.Univariate.NTT.Domain
 import CompPoly.Univariate.NTT.Evaluation
@@ -133,10 +135,23 @@ import CompPoly.Univariate.NTTFast.Plan
 import CompPoly.Univariate.Quotient.Core
 import CompPoly.Univariate.Quotient.Equiv
 import CompPoly.Univariate.Raw
+import CompPoly.Univariate.Raw.Context
 import CompPoly.Univariate.Raw.Core
 import CompPoly.Univariate.Raw.Division
+import CompPoly.Univariate.Raw.Modular
 import CompPoly.Univariate.Raw.Ops
 import CompPoly.Univariate.Raw.Proofs
+import CompPoly.Univariate.Roots
+import CompPoly.Univariate.Roots.Backend
+import CompPoly.Univariate.Roots.Context
+import CompPoly.Univariate.Roots.Correctness
+import CompPoly.Univariate.Roots.Enumeration
+import CompPoly.Univariate.Roots.Extraction
+import CompPoly.Univariate.Roots.RootProduct
+import CompPoly.Univariate.Roots.SmoothSubgroup
+import CompPoly.Univariate.Roots.SmoothSubgroup.Basic
+import CompPoly.Univariate.Roots.SmoothSubgroup.Correctness
+import CompPoly.Univariate.Roots.Splitter
 import CompPoly.Univariate.ToPoly
 import CompPoly.Univariate.ToPoly.Core
 import CompPoly.Univariate.ToPoly.Degree

CompPoly/Bivariate/ToPoly.lean

@@ -210,7 +210,7 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring
 /-- The outer coefficient of `toPoly p` is `CPolynomial.coeff p n` converted to `R[X]`. -/
 theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Semiring R]
     (p : CBivariate R) (n : ℕ) : (toPoly p).coeff n = (CPolynomial.coeff p n).toPoly := by
-      rw [ CBivariate.toPoly, Polynomial.finset_sum_coeff ]
+      rw [ CBivariate.toPoly, Polynomial.finsetSum_coeff ]
       rw [ Finset.sum_eq_single n ] <;> simp +contextual [ Polynomial.coeff_monomial ]
       simp_all +decide [ CPolynomial.mem_support_iff ]
       aesop
@@ -378,7 +378,7 @@ theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring
   simp only [Array.length_toList, Array.getElem?_toList]
   symm
   unfold CBivariate.toPoly
-  simp +decide [ Polynomial.eval_finset_sum ]
+  simp +decide [ Polynomial.eval_finsetSum ]
   rw [ Finset.sum_subset ]
   · exact fun i hi ↦ Finset.mem_range.mpr
       (Nat.lt_of_lt_of_le (Finset.mem_range.mp (Finset.mem_filter.mp hi |>.1)) (by simp))
@@ -468,7 +468,7 @@ theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semi
 theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     (f : CBivariate R) (j : ℕ) :
     (toPoly f).coeff j = CPolynomial.toPoly (f.val.coeff j) := by
-      erw [ Polynomial.finset_sum_coeff ]
+      erw [ Polynomial.finsetSum_coeff ]
       rw [ Finset.sum_eq_single j ] <;> simp +contextual [ Polynomial.coeff_monomial ]
       intro hj
       rw [ CPolynomial.support ] at hj
@@ -628,7 +628,7 @@ theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial
             Polynomial.eval a (∑ j ∈ s, g j * Polynomial.C (y ^ j)) =
               ∑ j ∈ s, Polynomial.eval a (g j) * y ^ j := by
       exact fun s g hg => by
-        rw [Polynomial.eval_finset_sum,
+        rw [Polynomial.eval_finsetSum,
           Finset.sum_congr rfl (fun j hj => h_eval_mul_C _ _ (hg j hj))]
     convert h_sum _ _ _
     · simp +decide [Polynomial.eval_eq_sum, Polynomial.sum_def]

CompPoly/Data/Array/Lemmas.lean

@@ -17,6 +17,16 @@ namespace Array
 
 variable {α : Type*} {unit : α}
 
+/-- Remove duplicates from an array while preserving first occurrences. -/
+def eraseDups [BEq α] (xs : Array α) : Array α :=
+  xs.foldl
+    (fun out x ↦
+      if out.contains x then
+        out
+      else
+        out.push x)
+    #[]
+
 /-- Checks if an array of elements from a type `R` is a boolean array, i.e., if every element is
   either `0` or `1`. -/
 def isBoolean {R : Type _} [Zero R] [One R] (a : Array R) : Prop :=
@@ -65,6 +75,68 @@ lemma getElem?_eq_toList {a : Array α} {i : ℕ} : a.toList[i]? = a[i]? := by
   rw (occs := .pos [2]) [← Array.toArray_toList (xs := a)]
   rw [List.getElem?_toArray]
 
+/-- `Array.map` and `getD` agree with indexed access on in-bounds indices. -/
+theorem getD_map_of_lt {β : Type*} (xs : Array α) (f : α → β)
+    (d : β) {i : Nat} (hi : i < xs.size) :
+    (xs.map f).getD i d = f xs[i] := by
+  rw [Array.getD_eq_getD_getElem?, Array.getElem?_map, Array.getElem?_eq_getElem hi]
+  simp
+
+theorem foldl_zipIdx_eq_foldl_toList_zipIdx {β : Type*}
+    (f : β → α × Nat → β) (init : β) (a : Array α) :
+    a.zipIdx.foldl f init = a.toList.zipIdx.foldl f init := by
+  cases a
+  simp
+
+theorem foldl_zipIdx_eq_foldl_toList_zipIdx_size {β : Type*}
+    (f : β → α × Nat → β) (init : β) (a : Array α) :
+    Array.foldl f init a.zipIdx 0 a.size = a.toList.zipIdx.foldl f init := by
+  cases a
+  simp
+
+theorem mem_foldl_append_of_mem {β : Type*}
+    (xs : Array α) (f : α → Array β) {x : α} {y : β}
+    (hx : x ∈ xs.toList) (hy : y ∈ (f x).toList) :
+    y ∈ (xs.foldl (fun out x ↦ out ++ f x) #[]).toList := by
+  cases xs with
+  | mk data =>
+      simp at hx ⊢
+      have haux : ∀ (data : List α) (acc : Array β),
+          y ∈ acc.toList ∨ (∃ x, x ∈ data ∧ y ∈ (f x).toList) →
+            y ∈ (data.foldl (fun out x ↦ out ++ f x) acc).toList := by
+        intro data
+        induction data with
+        | nil =>
+            intro acc h
+            simp at h ⊢
+            exact h
+        | cons z zs ih =>
+            intro acc h
+            simp only [List.foldl_cons]
+            apply ih
+            rcases h with hacc | ⟨x, hx, hyx⟩
+            · left
+              simp [hacc]
+            · simp only [List.mem_cons] at hx
+              cases hx with
+              | inl hxz =>
+                  subst x
+                  left
+                  simp [hyx]
+              | inr hxzs =>
+                  right
+                  exact ⟨x, hxzs, hyx⟩
+      simpa using haux data #[] (Or.inr ⟨x, hx, hy⟩)
+
+theorem mem_flatten_map_of_mem {β : Type*}
+    (xs : Array α) (f : α → Array β) {x : α} {y : β}
+    (hx : x ∈ xs.toList) (hy : y ∈ (f x).toList) :
+    y ∈ (xs.map f).flatten := by
+  cases xs with
+  | mk data =>
+      simp at hx hy ⊢
+      exact ⟨x, hx, hy⟩
+
 attribute [simp] Array.getElem?_eq_getElem
 
 -- @[simp] theorem matchSize_comm (a : Array α) (b : Array α) (unit : α) :

CompPoly/Data/List/Lemmas.lean

@@ -29,6 +29,19 @@ theorem append_getLast_dropLast {α : Type u} (l : List α) (h : l ≠ []) :
       simp only [cons_append, cons.injEq, true_and]
       apply ih
 
+theorem foldl_congr_of_mem {α : Type u} {β : Type v} {f g : α → β → α}
+    (xs : List β) (acc : α) (h : ∀ acc' x, x ∈ xs → f acc' x = g acc' x) :
+    xs.foldl f acc = xs.foldl g acc := by
+  induction xs generalizing acc with
+  | nil =>
+      simp
+  | cons x xs ih =>
+      simp only [foldl_cons]
+      rw [h acc x (by simp)]
+      apply ih
+      intro acc' y hy
+      exact h acc' y (by simp [hy])
+
 theorem foldl_split_outer {α : Type u} {β : Type v} (f : α → β → α) (init : α)
     (l : List β) (h : l ≠ []): foldl (f:=f) (init:=init) (l)
     = f (foldl (f:=f) (init:=init) (l.dropLast)) (l.getLast (by omega)) := by

CompPoly/Data/Nat/Bitwise.lean

@@ -547,9 +547,8 @@ lemma sum_eq_xor_plus_twice_and (n : Nat) : ∀ m : ℕ, n + m = (n ^^^ m) + 2 *
     rw [zero_add, Nat.zero_and, mul_zero, add_zero, Nat.zero_xor]
   | bit bn n2 ih =>
     intro m
-    let resDiv2M := Nat.boddDiv2 m
-    let bm := resDiv2M.fst
-    let m2 := resDiv2M.snd
+    let bm := Nat.bodd m
+    let m2 := Nat.div2 m
     have h_m2 : m2 = Nat.div2 m := by
       rfl
     have h_bm : bm = Nat.bodd m := by
@@ -1295,7 +1294,7 @@ lemma getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary: ∀ j
   induction n with
   | zero =>
     intro k;
-    simp only [Nat.pow_zero, Fin.val_eq_zero, not_lt_zero', ↓reduceDIte]
+    simp only [Nat.pow_zero, Fin.val_eq_zero, Nat.not_lt_zero, ↓reduceDIte]
     exact getBit_zero_eq_zero
   | succ n ih =>
     -- Inductive step: Assume the property holds for `n`, prove it for `n+1`.

CompPoly/Data/Polynomial/MonomialBasis.lean

@@ -64,7 +64,7 @@ noncomputable def monomialBasisOfDegreeLT {n : ℕ} : Basis (Fin n) L (L⦃< n
       simp only [SetLike.mk_smul_mk]
       conv =>
         lhs
-        simp only [Finsupp.sum, AddSubmonoidClass.coe_finset_sum, finset_sum_coeff, coeff_smul,
+        simp only [Finsupp.sum, AddSubmonoidClass.coe_finsetSum, finsetSum_coeff, coeff_smul,
           coeff_X_pow, smul_eq_mul, mul_ite, mul_one, mul_zero, monomials_in_submodule, v]
       -- ⊢ (∑ x ∈ l.support, if ↑i = ↑x then l x else 0) = l i
       simp_rw [Fin.val_eq_val, eq_comm]
@@ -110,7 +110,7 @@ noncomputable def monomialBasisOfDegreeLT {n : ℕ} : Basis (Fin n) L (L⦃< n
         -- we have to convert (↑p).sum into Fin n → L form using Polynomial.sum_fin
         simp only [monomial_zero_right, implies_true, ←Polynomial.sum_fin (hn := h_deg_p)]
       -- ⊢ ↑(∑ i, c i • monomials_in_submodule i) = ∑ i, (monomial ↑i) ((↑p).coeff ↑i)
-      rw [AddSubmonoidClass.coe_finset_sum] -- bring both sides back to L[X]
+      rw [AddSubmonoidClass.coe_finsetSum] -- bring both sides back to L[X]
       apply Finset.sum_congr rfl
       intro ⟨i, hi_finN⟩ hi
       simp only [SetLike.mk_smul_mk, c, monomials_in_submodule]

CompPoly/Data/RingTheory/AlgebraTower.lean

@@ -61,7 +61,7 @@ instance AlgebraTower.toIsScalarTower (a : AlgebraTower C) {i j k : ι}
       simp only [map_mul]
       rw [←RingHom.comp_apply]
       unfold instIJ instJK instIK AlgebraTower.toAlgebra
-      simp_rw [algebraMap, Algebra.algebraMap]
+      simp_rw [RingHom.algebraMap_toAlgebra]
       have h_assoc := a.coherence' (i:=i) (j:=j) (k:=k) (h1:=h1) (h2:=h2)
       rw [h_assoc]
       rw [mul_assoc]
@@ -123,8 +123,7 @@ def AlgebraTowerEquiv.toAlgEquivOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
     commutes' := fun r => by
       simp only [RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
       unfold instAij instAiBij
-      rw [algebraMap, algebraMap, Algebra.algebraMap, Algebra.algebraMap,AlgebraTower.toAlgebra,
-        AlgebraTowerEquiv.toAlgebraOverLeft, AlgebraTowerEquiv.algebraMapRightUp]
+      simp only [AlgebraTowerEquiv.algebraMapRightUp, RingHom.algebraMap_toAlgebra]
       simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
       exact Eq.symm (e.commutesLeft' i j h r)
     map_mul' := fun x y => by

CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean

@@ -277,7 +277,7 @@ lemma getSDomainBasisCoeff_of_sum_repr [NeZero R_rate] (i : Fin (ℓ + 1))
       simp only [Basis.repr_self]
     have hx_at_j_simplified :
         (∑ j_x, x_coeffs j_x • (b.repr (b j_x))) j = x_coeffs j := by
-      simp only [h_repr_basis, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_finset_sum,
+      simp only [h_repr_basis, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_finsetSum,
         Finset.sum_apply, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte]
     let x_coeffs_fs := Finsupp.equivFunOnFinite.symm x_coeffs
     let rhs_sum := ∑ j_x, (x_coeffs_fs j_x) • (b j_x)

CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean

@@ -189,7 +189,7 @@ lemma βᵢ_not_in_Uᵢ (i : Fin r) :
       omega
     else
       push Not at h_i
-      have h_i_eq_0: i = 0 := by exact Fin.le_zero_iff'.mp h_i
+      have h_i_eq_0: i = 0 := by exact nonpos_iff_eq_zero.mp h_i
       have set_empty: Set.Ico 0 i = ∅ := by
         rw [h_i_eq_0]
         simp only [Set.Ico_eq_empty_iff]

CompPoly/Fields/Binary/Common.lean

@@ -360,7 +360,7 @@ lemma toPoly_ne_zero_iff_ne_zero {w : Nat} (v : BitVec w) :
     have h_coeff_formula : ∀ i : Fin w, (toPoly v).coeff i.val = if v.getLsb i then 1 else 0 := by
       intro i
       unfold toPoly
-      rw [finset_sum_coeff]
+      rw [finsetSum_coeff]
       have h_ite: ∀ b : Fin w, (if v.getLsb b then (X : (ZMod 2)[X])^b.val else 0).coeff i.val =
           if v.getLsb b then (if b = i then 1 else 0) else 0 := by
         intro b
@@ -470,7 +470,7 @@ lemma BitVec_lt_two_pow_of_toPoly_degree_lt {w d : ℕ} (v : BitVec w)
     have h_i_lt_w : i < w := by omega
     have h_coeff_one : (toPoly v).coeff i = 1 := by
       unfold toPoly
-      rw [finset_sum_coeff]
+      rw [finsetSum_coeff]
       rw [Finset.sum_eq_single ⟨i, h_i_lt_w⟩]
       · have h_getLsb_eq_testBit : v.getLsb ⟨i, h_i_lt_w⟩ = v.toNat.testBit i := by
           rfl
@@ -627,7 +627,7 @@ theorem toPoly_coeff {w : ℕ} (v : BitVec w) (n : ℕ) :
       (if h : n < w then (if v.getLsb ⟨n, h⟩ = true then (1 : ZMod 2) else 0) else 0) := by
   classical
   unfold toPoly
-  rw [Polynomial.finset_sum_coeff]
+  rw [Polynomial.finsetSum_coeff]
   by_cases h : n < w
   · -- case n < w
     simp only [dif_pos h]
@@ -667,7 +667,7 @@ theorem toPoly_coeff {w : ℕ} (v : BitVec w) (n : ℕ) :
         intro hi0_not
         simp [Finset.mem_univ] at hi0_not
     -- conclude
-    simpa [Polynomial.finset_sum_coeff, i0] using hmain
+    simpa [Polynomial.finsetSum_coeff, i0] using hmain
   · -- case ¬ n < w
     simp only [dif_neg h]
     -- show every summand has coefficient 0

CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean

@@ -240,7 +240,6 @@ lemma algebra_adjacent_tower_eq_AdjoinRoot_algebra (k : ℕ) :
   rw [algebra_adjacent_tower_def]
   unfold canonicalEmbedding
   rw [←AdjoinRoot.algebraMap_eq]
-  rw [algebraMap, Algebra.algebraMap]
   exact
     Algebra.algebra_ext (AdjoinRoot.instAlgebra (poly k)).2.toAlgebra
       (AdjoinRoot.instAlgebra (poly k)) (congrFun rfl)

CompPoly/Fields/Binary/Tower/Abstract/Basis.lean

@@ -174,7 +174,7 @@ lemma algebraMap_𝕏_eq_of_index_eq (r k m : ℕ) (h_k_le : k + 1 ≤ r) (h_m_l
     (h_eq : k = m) :
     letI := binaryAlgebraTower (l := k + 1) (r := r) (h_le := h_k_le)
     letI := binaryAlgebraTower (l := m + 1) (r := r) (h_le := h_m_le)
-    (Algebra.algebraMap (𝕏 k) : BTField r) = (Algebra.algebraMap (𝕏 m) : BTField r) := by
+    (algebraMap _ _ (𝕏 k) : BTField r) = (algebraMap _ _ (𝕏 m) : BTField r) := by
   subst h_eq
   rfl
 
@@ -302,13 +302,11 @@ theorem multilinearBasis_apply (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) → ∀
       simp_rw [algebraMap.coe_pow] -- rhs
       simp_rw [algebraMap.coe_prod] -- lhs
       unfold Algebra.cast
-      rw! (castMode:=.all) [←algebraMap]
       conv_lhs =>
         rw [←Fin.prod_congr' (b:=r1-l) (a:=prevDiff) (h:=by omega)]
         simp only [Fin.val_cast]
-      simp (config := { failIfUnchanged := false }) only [algebraMap, instAlgebraSucc]
-      erw [RingHom.map_pow]
-      simp (config := { failIfUnchanged := false }) only [←binaryTowerAlgebra_apply_assoc]
+      simp only [RingHom.map_pow]
+      simp only [←binaryTowerAlgebra_apply_assoc]
       ------------------ Equality of bit-based powers of generators -----------------
       --- The outtermost term
       have hfinProd_msb := bit_revFinProdFinEquiv_symm_2_pow_succ (n:=prevDiff)

CompPoly/Fields/Binary/Tower/Abstract/Split.lean

@@ -149,10 +149,10 @@ theorem mul_join_via_add_smul (k : ℕ) (h_pos : k > 0) (a₁ a₀ b₁ b₀ : B
 
   have h_a₁_b₀_Z_k : (algebraMap (BTField (k - 1)) (BTField k)) b₀ * a₁ • Z k
     = (a₁ * b₀) • Z k := by
-    rw [Algebra.smul_def', ←algebraMap, ←mul_assoc, ←map_mul, ←Algebra.smul_def, mul_comm]
+    rw [Algebra.smul_def', ←mul_assoc, ←map_mul, ←Algebra.smul_def, mul_comm]
   have h_a₀_b₁_Z_k :  (algebraMap (BTField (k - 1)) (BTField k)) a₀ * b₁ • Z k
     = (a₀ * b₁) • Z k := by
-    rw [Algebra.smul_def', ←algebraMap, ←mul_assoc, ←map_mul, ←Algebra.smul_def, mul_comm]
+    rw [Algebra.smul_def', ←mul_assoc, ←map_mul, ←Algebra.smul_def, mul_comm]
   have h_Z_k_pow_2 : (Z k) ^ 2 = Z (k - 1) • Z k + 1 := by
     rw [sumZeroIffEq (x:=(Z k)^2) (y:=Z (k - 1) • Z k + 1).mp]
     rw [←add_assoc]
@@ -161,7 +161,6 @@ theorem mul_join_via_add_smul (k : ℕ) (h_pos : k > 0) (a₁ a₀ b₁ b₀ : B
     rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h
     simp only [eq_mp_eq_cast] at h
     convert h
-    rw [Algebra.algebraMap]
     conv_lhs =>
       simp only [instAlgebra];
       change (towerAlgebraMap (l:=k-1) (r:=k) (h_le:=by omega)) (Z (k - 1))
@@ -307,9 +306,9 @@ lemma split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1))
   apply h.mp
   -- ⊢ mappedVal = join_via_add_smul h_pos 0 x
   unfold mappedVal
-  rw [algebraMap, Algebra.algebraMap]
-  unfold instAlgebra binaryAlgebraTower
-  rw [AlgebraTower.toAlgebra, AlgebraTower.algebraMap, instAlgebraTowerNatBTField]
+  unfold instAlgebra binaryAlgebraTower AlgebraTower.toAlgebra
+  simp only [RingHom.algebraMap_toAlgebra]
+  rw [AlgebraTower.algebraMap, instAlgebraTowerNatBTField]
   simp only
   have h_concrete_embedding_succ_1 := towerAlgebraMap_succ_1 (k:=k-1)
   rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h_concrete_embedding_succ_1
@@ -327,12 +326,11 @@ lemma split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1))
   have h := algebraMap_adjacent_tower_def (l:=k-1)
   rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h
   simp only [eqRec_eq_cast] at h
-  rw [algebraMap, Algebra.algebraMap] at ⊢ h
   rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h
   simp only [cast_eq] at h
   unfold binaryAlgebraTower AlgebraTower.toAlgebra AlgebraTower.algebraMap
     instAlgebraTowerNatBTField
-  simp only [] -- normalize eqRec before rewrite
+  simp only [RingHom.algebraMap_toAlgebra] -- unfold algebraMap (v4.30: no longer rw-unfoldable)
   -- Both sides reduce to (cast ⋯ (canonicalEmbedding (k-1))) x through different paths
   erw [h_concrete_embedding_succ_1]; simp only [eqRec_eq_cast]
 

CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean

@@ -234,9 +234,9 @@ lemma split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField
   apply h
   -- ⊢ mappedVal = join h_pos zero x
   unfold mappedVal
-  rw [algebraMap, Algebra.algebraMap]
-  unfold instAlgebra ConcreteBTFieldAlgebra
-  rw [AlgebraTower.toAlgebra, AlgebraTower.algebraMap, instAlgebraTowerConcreteBTF]
+  unfold instAlgebra ConcreteBTFieldAlgebra AlgebraTower.toAlgebra
+  simp only [RingHom.algebraMap_toAlgebra]
+  rw [AlgebraTower.algebraMap, instAlgebraTowerConcreteBTF]
   simp only
   have h_concrete_embedding_succ_1 := concreteTowerAlgebraMap_succ_1 (k:=k-1)
   rw! (castMode:=.all) [Nat.sub_one_add_one (by omega)] at h_concrete_embedding_succ_1
@@ -439,8 +439,7 @@ lemma aeval_definingPoly_at_Z_succ (k : ℕ) :
   -- Z_square_mul_form uses instAlgebraLiftConcreteBTField internally
   rw [Z_square_mul_form (k:=k) (prev:=(getBTFResult (k:=k)))]
   rw [add_assoc]
-  rw [algebraMap, Algebra.algebraMap, instAlgebraLiftConcreteBTField]
-  simp only
+  simp only [RingHom.algebraMap_toAlgebra]
   -- f uses ConcreteBTFieldAlgebra, it's same as instAlgebraLiftConcreteBTField at step = 1
   rw [h_f_is_canonical_embedding, concreteTowerAlgebraMap_succ_1]
   simp only [canonicalAlgMap]; rw [mul_comm]