feat: bump lean version

CompPoly/Bivariate/ToPoly.lean

@@ -49,7 +49,7 @@ noncomputable def toPoly {R : Type*} [BEq R] [LawfulBEq R] [Semiring R]
   Extracts each Y-coefficient via `p.coeff`, converts to `CPolynomial R` via
   `toImpl` and trimming, then builds the canonical bivariate sum.
   -/
-def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
+noncomputable def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     [DecidableEq R] (p : R[X][Y]) : CBivariate R :=
   (p.support).sum (fun j ↦
     let cj := p.coeff j
@@ -171,9 +171,10 @@ lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
               (show q.support ⊆ p.support ∪ q.support from Finset.subset_union_right) ]
           · rw [ ← Finset.sum_add_distrib ]
             refine' Finset.sum_congr rfl fun x hx ↦ _
-            rw [ ← CPolynomial.monomial_add ]
-            congr
-            exact Eq.symm (toImpl_add (p.coeff x) (q.coeff x))
+            erw [ ← CPolynomial.monomial_add ]
+            congr 1
+            apply Subtype.ext
+            exact (toImpl_add (p.coeff x) (q.coeff x)).symm
           · aesop
           · aesop
         · aesop
@@ -195,7 +196,8 @@ theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring
         unfold CBivariate.ofPoly
         induction' p.support using Finset.induction with j s hj ih
         · exact CPolynomial.eq_iff_coeff.mpr (congrFun rfl)
-        · rw [ Finset.sum_insert hj, CPolynomial.coeff_add, ih, Finset.sum_insert hj ]
+        · rw [Finset.sum_insert hj]
+          erw [CPolynomial.coeff_add, ih, Finset.sum_insert hj]
       rw [ h_coeff_sum, Finset.sum_eq_single n ]
       · rw [ CPolynomial.coeff_monomial ]
         simp +decide [ CPolynomial.toPoly ]
@@ -237,7 +239,8 @@ theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     toPoly (p * q) = toPoly p * toPoly q := by
       have h_mul : (p * q).toPoly =
           (CPolynomial.toPoly (p * q)).map (CPolynomial.ringEquiv (R := R)) := toPoly_eq_map (p * q)
-      rw [ h_mul, CPolynomial.toPoly_mul ]
+      rw [ h_mul ]
+      erw [CPolynomial.toPoly_mul]
       rw [ Polynomial.map_mul, ← toPoly_eq_map, ← toPoly_eq_map ]
 
 end ToPolyCore
@@ -310,6 +313,8 @@ lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R]
     ofPoly (0 : R[X][Y]) = 0 := by
       unfold CBivariate.ofPoly
       simp +decide [ Polynomial.support ]
+      erw [Finsupp.support_zero]
+      exact Finset.sum_empty
 
 /-- Ring hom from computable bivariates to Mathlib bivariates. -/
 noncomputable def toPolyRingHom
@@ -743,7 +748,7 @@ theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semi
       CPolynomial.coeff (swap (R := R) f) j =
         ∑ x ∈ f.supportY, CPolynomial.monomial x ((f.val.coeff x).coeff j) := by
     unfold CBivariate.swap CBivariate.supportY
-    rw [hCoeffSumOuter]
+    erw [hCoeffSumOuter]
     exact Finset.sum_congr rfl (fun x hx => hInner x)
   change CPolynomial.coeff (CPolynomial.coeff (swap (R := R) f) j) i =
     CPolynomial.coeff (CPolynomial.coeff f i) j

CompPoly/Data/Nat/Bitwise.lean

@@ -35,7 +35,7 @@ lemma ENat.le_floor_NNReal_iff (x : ENat) (y : ℝ≥0) (hx_ne_top : x ≠ ⊤)
     (x : ENat) ≤ ((Nat.floor y) : ENat) ↔ x.toNat ≤ Nat.floor y := by
   lift x to ℕ using hx_ne_top
   -- y : ℝ≥0, x : ℕ, ⊢ ↑x ≤ ↑⌊y⌋₊ ↔ (↑x).toNat ≤ ⌊y⌋₊
-  simp only [Nat.cast_le, toNat_coe]
+  simp only [ENat.coe_le_coe, toNat_coe]
 
 section ENNReal
 open ENNReal
@@ -49,29 +49,11 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0}
 -- lemma ENNReal.div_lt_div_right (hc₀ : c ≠ 0) (hc : c ≠ ∞) (hab : a < b) : a / c < b / c :=
 --   (ENNReal.div_lt_div_iff_left hc₀ hc).2 hab
 
-theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
-    ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ := by
--- Let x = ↑a and y = ↑b for readability
-  let x : ENNReal := a
-  let y : ENNReal := b
-  -- Prove x and y are non-zero and finite (needed for inv_cancel)
-  have hx_ne_zero : x ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
-  have hy_ne_zero : y ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
-  have hx_ne_top : x ≠ ∞ := by exact ENNReal.natCast_ne_top a
-  have hy_ne_top : y ≠ ∞ := by exact ENNReal.natCast_ne_top b
-  have ha_NNReal_ne0 : (a : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr ha
-  have hb_NNReal_ne0 : (b : ℝ≥0) ≠ 0 := by exact Nat.cast_ne_zero.mpr hb
-  -- (a * b)⁻¹ = b⁻¹ * a⁻¹
-  have hlhs : ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ℝ≥0)⁻¹ * (b : ℝ≥0)⁻¹) := by
-    rw [coe_inv (hr := by exact ha_NNReal_ne0)]
-    rw [coe_inv (hr := by exact hb_NNReal_ne0)]
-    rw [ENNReal.coe_natCast, ENNReal.coe_natCast]
-  have hrhs : ((a : ENNReal) * (b : ENNReal))⁻¹ = ((a : ℝ≥0) * (b : ℝ≥0))⁻¹ := by
-    rw [coe_inv (hr := (mul_ne_zero_iff_right hb_NNReal_ne0).mpr (ha_NNReal_ne0))]
-    simp only [coe_mul, coe_natCast]
-  rw [hlhs, hrhs]
-  rw [mul_inv_rev (a := (a : ℝ≥0)) (b := (b : ℝ≥0))]
-  rw [coe_mul, mul_comm]
+theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) :
+    ((a : ENNReal)⁻¹ * (b : ENNReal)⁻¹) = ((a : ENNReal) * (b : ENNReal))⁻¹ :=
+  (ENNReal.mul_inv
+    (Or.inl (Nat.cast_ne_zero.mpr ha))
+    (Or.inl (ENNReal.natCast_ne_top a))).symm
 
 lemma ENNReal.coe_le_of_NNRat {a b : ℚ≥0} : ((a : ENNReal)) ≤ (b) ↔ a ≤ b := by
   exact ENNReal.coe_le_coe.trans (by norm_cast)

CompPoly/Data/Polynomial/Frobenius.lean

@@ -486,7 +486,7 @@ theorem degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X
     have h_exponent_dvd : Monoid.exponent Kˣ ∣ q ^ n - 1 :=
       Monoid.exponent_dvd_of_forall_pow_eq_one h_units_pow_eq_one
     have h_order_K : Fintype.card Kˣ = q ^ d - 1 := by
-      rw [Fintype.card_units, h_card_K]
+      erw [Fintype.card_units, h_card_K]
     have h_exp_eq_order : Monoid.exponent Kˣ = Fintype.card Kˣ := by
       rw [IsCyclic.exponent_eq_card, Nat.card_eq_fintype_card]
     rw [h_exp_eq_order, h_order_K] at h_exponent_dvd

CompPoly/Data/RingTheory/AlgebraTower.lean

@@ -41,7 +41,7 @@ variable {ι : Type*} [Preorder ι]
   {B : ι → Type*} [∀ i, CommSemiring (B i)] [AlgebraTower B]
   {C : ι → Type*} [∀ i, CommSemiring (C i)] [AlgebraTower C]
 
-@[simp]
+@[simp, reducible]
 def AlgebraTower.toAlgebra {i j : ι} (h : i ≤ j) : Algebra (A i) (A j) :=
   (AlgebraTower.algebraMap (i:=i) (j:=j) (h:=h)).toAlgebra
 
@@ -102,11 +102,11 @@ def AlgebraTowerEquiv.algebraMapLeftUp (e : AlgebraTowerEquiv A B) (i j : ι)
   have hjRingEquiv: RingEquiv (B i) (A i) := (e.toRingEquiv i).symm
   exact hAij.comp hjRingEquiv.toRingHom
 
-def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
+@[reducible] def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
     (h : i ≤ j) : Algebra (A i) (B j) := by
   exact (e.algebraMapRightUp i j h).toAlgebra
 
-def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι)
+@[reducible] def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι)
     (h : i ≤ j) : Algebra (B i) (A j) := by
   exact (e.algebraMapLeftUp i j h).toAlgebra
 

CompPoly/Data/Vector/Basic.lean

@@ -89,7 +89,7 @@ lemma cons_empty_tail_eq_nil {α} (hd : α) (tl : Vector α 0) :
 theorem tail_cons {α} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).tail = tl := by
   rw [cons, Vector.insertIdx]
   simp only [Nat.add_one_sub_one, Array.insertIdx_zero, tail_eq_cast_extract, extract_mk,
-    Array.extract_append, List.extract_toArray, List.extract_eq_drop_take, add_tsub_cancel_right,
+    Array.extract_append, List.extract_toArray, List.extract_eq_take_drop, add_tsub_cancel_right,
     List.drop_succ_cons, List.drop_nil, List.take_nil, List.size_toArray, List.length_cons,
     List.length_nil, tsub_self, Array.take_eq_extract, Array.empty_append, cast_mk, mk_eq,
     Array.extract_eq_self_iff, size_toArray, le_refl, and_self, or_true]

CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean

@@ -501,12 +501,13 @@ theorem additiveNTT_correctness (h_ℓ : ℓ ≤ r)
   have res := output_foldl_correctness j
   unfold output_foldl at res
   simp only [Fin.zero_eta, Nat.sub_zero, pow_zero, Nat.div_one, Fin.eta,
-    Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue, base_coeffsBySuffix] at res
+    Nat.pow_zero, Nat.getLowBits_zero_eq_zero (n := j.val), Fin.isValue] at res
   simp only [←
     intermediate_poly_P_base 𝔽q β h_ℓ_add_R_rate
       h_ℓ original_coeffs,
     Fin.zero_eta]
-  rw [← res]
+  erw [base_coeffsBySuffix] at res
+  erw [← res]
   simp_rw [Nat.sub_right_comm]
 
 end AlgorithmCorrectness

CompPoly/Fields/Binary/AdditiveNTT/Impl.lean

@@ -399,7 +399,7 @@ abbrev BTF₃ := ConcreteBTField 3 -- 8 bits
 instance : NeZero (2^3) := ⟨by norm_num⟩
 instance : Field BTF₃ := instFieldConcrete
 instance : DecidableEq BTF₃ := (inferInstance : DecidableEq (ConcreteBTField 3))
-instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3))
+noncomputable instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3))
 
 /-- Test of the computable additive NTT over BTF₃ (an 8-bit binary tower field `BTF₃`).
 **Input polynomial:** p(x) = x (novel coefficients [7, 1, 0, 0]) of size `2^ℓ` in `BTF₃`

CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean

@@ -380,7 +380,7 @@ lemma getSDomainBasisCoeff_of_iteratedQuotientMap
           simp only [zero_add]
           omega⟩)
       simp only [Fin.zero_eta, Fin.coe_ofNat_eq_mod, Nat.sub_zero] at h_interW_comp
-      rw [h_interW_comp]
+      erw [h_interW_comp]
       have h_index : 0 + i.val = i.val := by omega
       rw! (castMode := .all) [h_index]
       rfl
@@ -480,7 +480,7 @@ theorem base_intermediateNovelBasisX (j : Fin (2 ^ ℓ)) :
   simp only [Fin.mk_zero'] at h_res
   conv_lhs =>
     enter [2, x, 1]
-    rw [h_res ⟨x, by omega⟩]
+    erw [h_res ⟨x, by omega⟩]
   congr
 
 omit [DecidableEq L] [DecidableEq 𝔽q] h_Fq_char_prime hF₂ hβ_lin_indep h_β₀_eq_1 in

CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean

@@ -368,7 +368,7 @@ lemma W₀_eq_X : W 𝔽q β 0 = X := by
   rw [W]
   have : (univ : Finset (U 𝔽q β 0)) = {0} := by
     ext x
-    simp only [U, Set.Ico, mem_univ, mem_singleton, true_iff]
+    simp only [mem_univ, mem_singleton, true_iff]
     --x : ↥(U 𝔽q β 0), ⊢ x = 0
     unfold U at x
     have h_empty : Set.Ico 0 (0: Fin r) = ∅ := by
@@ -1340,11 +1340,19 @@ lemma degree_Xⱼ (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) :
     -- We use the `Nat.digits` API for this.
     rw [Finset.sum_congr rfl deg_each] -- .degree introduces (WithBot ℕ)
     -- ⊢ ⊢ ∑ x, ↑(if bit ↑x ↑j = 1 then 2 ^ ↑x else 0) = ↑↑j
-    set f:= fun x: ℕ => if Nat.getBit x j = 1 then (2: ℕ) ^ (x: ℕ) else 0
-    norm_cast -- from WithBot ℕ to ℕ
-    change (∑ x : Fin ℓ, f x) = (j.val: WithBot ℕ)
-    norm_cast
-    -- ⊢ (∑ x ∈ Icc 0 (ℓ - 1), if bit x j = 1 then 2 ^ x else 0) = ↑j => in Withbot ℕ
+    -- The goal is: ∑ x, ↑(if ... then 2^↑x else 0) = ↑↑j in WithBot ℕ
+    -- Reduce to ℕ equality via suffices and cast lemma
+    set f := fun x : ℕ => if Nat.getBit x j = 1 then (2 : ℕ) ^ x else 0
+    suffices h : (∑ x : Fin ℓ, f x.val) = j.val by
+      simp only [f] at h
+      have h2 := congrArg (fun n : ℕ => (n : WithBot ℕ)) h
+      simp only [Nat.cast_sum, Nat.cast_ite, Nat.cast_pow, Nat.cast_ofNat,
+        Nat.cast_zero] at h2
+      convert h2 using 1
+      apply Finset.sum_congr rfl
+      intro x _
+      simp only [Nat.cast_ite, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_zero]
+    -- ⊢ (∑ x, f x.val) = j.val in ℕ
     rw [Fin.sum_univ_eq_sum_range (n:=ℓ)] -- switch to sum over Finset.range ℓ
     have h_range: range ℓ = Icc 0 (ℓ-1) := by
       rw [←Nat.range_succ_eq_Icc_zero (n:=ℓ - 1)]
@@ -1385,10 +1393,6 @@ noncomputable def basisVectors (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
 /-- The vector space of coefficients for polynomials of degree < 2^ℓ. -/
 abbrev CoeffVecSpace (L : Type u) (ℓ : Nat) := Fin (2^ℓ) → L
 
-noncomputable instance (ℓ : Nat) : AddCommGroup (CoeffVecSpace L ℓ) := by
-  unfold CoeffVecSpace
-  infer_instance -- default additive group for `Fin (2^ℓ) → L`
-
 noncomputable instance finiteDimensionalCoeffVecSpace (ℓ : ℕ) :
   FiniteDimensional (K := L) (V := CoeffVecSpace L ℓ) := by
   unfold CoeffVecSpace
@@ -1398,7 +1402,10 @@ noncomputable instance finiteDimensionalCoeffVecSpace (ℓ : ℕ) :
 def toCoeffsVec (ℓ : Nat) : L⦃<2^ℓ⦄[X] →ₗ[L] CoeffVecSpace L ℓ where
   toFun := fun p => fun i => p.val.coeff i.val
   map_add' := fun p q => by ext i; simp [coeff_add]
-  map_smul' := fun c p => by ext i; simp [coeff_smul, smul_eq_mul]
+  map_smul' := fun c p => by
+    ext i
+    simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul]
+    rw [Submodule.coe_smul, Polynomial.coeff_smul, smul_eq_mul]
 
 /-- The rows of a square lower-triangular matrix with
 non-zero diagonal entries are linearly independent. -/

CompPoly/Fields/Binary/BF128Ghash/Basic.lean

@@ -189,7 +189,8 @@ def root : BF128Ghash := AdjoinRoot.root ghashPoly
 theorem root_satisfies_poly : root^128 + root^7 + root^2 + root + 1 = 0 := by
   unfold root ghashPoly
   have h := AdjoinRoot.eval₂_root ghashPoly
-  simp only [ghashPoly, eval₂_add, eval₂_pow, eval₂_X, eval₂_one] at h
+  simp only [ghashPoly, eval₂_add, eval₂_X, eval₂_one] at h
+  erw [eval₂_pow, eval₂_X, eval₂_pow, eval₂_X, eval₂_pow, eval₂_X] at h
   exact h
 
 /-- BF128Ghash is a finite type. -/

CompPoly/Fields/Binary/Common.lean

@@ -556,13 +556,12 @@ lemma toPoly_128_extend_256 (a : B128) :
   intro (i : Fin (128)) hi_mem_univ
   dsimp only [BitVec.getLsb]
   simp_rw [to256_toNat]
-  simp only [Fin.val_castAdd, Fin.val_addNat, add_eq_left, ite_eq_right_iff, ne_eq,
-    Nat.add_eq_zero_iff, Fin.val_eq_zero_iff, Fin.isValue, OfNat.ofNat_ne_zero, and_false,
-    not_false_eq_true, pow_eq_zero_iff, X_ne_zero, imp_false, Bool.not_eq_true]
-  -- ⊢ (BitVec.toNat a).testBit (↑i + 128) = false
-  apply Nat.testBit_lt_two_pow
+  simp only [Fin.val_castAdd, Fin.val_addNat]
   have h_toNat_lt := BitVec.toNat_lt_twoPow_of_le (n := i.val + 128) (x := a) (h := by omega)
-  exact h_toNat_lt
+  have h_testBit_false : (BitVec.toNat a).testBit (↑i + 128) = false :=
+    Nat.testBit_lt_two_pow h_toNat_lt
+  simp only [h_testBit_false, Bool.false_eq_true, ↓reduceIte, add_zero]
+  rfl
 
 -- Lemma: Left Shift corresponds to Multiplication by X^k
 theorem BitVec_getLsb_eq_false_of_toNat_lt_two_pow {w d : ℕ} (a : BitVec w) (ha : a.toNat < 2 ^ d)

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

@@ -83,9 +83,8 @@ lemma towerAlgebraMap_succ_1 (k : ℕ) :
     towerAlgebraMap (l:=k) (r:=k+1) (h_le:=by omega) = canonicalEmbedding k := by
   unfold towerAlgebraMap
   simp only [Nat.left_eq_add, one_ne_zero, ↓reduceDIte,
-    Nat.add_one_sub_one, eq_mp_eq_cast, cast_eq]
-  rw [towerAlgebraMap_id]
-  rw [RingHom.comp_id]
+    Nat.add_one_sub_one, eq_mp_eq_cast]
+  erw [cast_eq, towerAlgebraMap_id, RingHom.comp_id]
 
 /-! Right associativity of the Tower Map -/
 lemma towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) :
@@ -96,8 +95,8 @@ lemma towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) :
   conv_lhs => rw [towerAlgebraMap]
   have h_l_ne_eq_r_add_1 : l ≠ r + 1 := by omega
   simp only [h_l_ne_eq_r_add_1, ↓reduceDIte, Nat.add_one_sub_one,
-    eq_mp_eq_cast, cast_eq, RingHom.coe_comp, Function.comp_apply]
-  rw [towerAlgebraMap_succ_1]
+    eq_mp_eq_cast, RingHom.coe_comp, Function.comp_apply]
+  erw [cast_eq, towerAlgebraMap_succ_1]; congr 1
 
 /-! Left associativity of the Tower Map -/
 theorem towerAlgebraMap_succ_last (r : ℕ) : ∀ l : ℕ, (h_le : l ≤ r) →
@@ -136,7 +135,7 @@ theorem BTField.RingHom_comp_cast {α β γ δ : ℕ} (f : BTField α →+* BTFi
   have h_heq : HEq ((cast (h1) g).comp f) (cast (h2) (g.comp f)) := by
     subst h -- this simplifies h1 h2 in cast which makes them trivial equality
       -- => hence it becomes easier to simplify
-    simp only [BTField, BTFieldIsField, cast_eq, heq_eq_eq]
+    simp only [BTField, cast_eq, heq_eq_eq]
   apply eq_of_heq h_heq
 
 theorem towerAlgebraMap_assoc : ∀ r mid l : ℕ, (h_l_le_mid : l ≤ mid) → (h_mid_le_r : mid ≤ r) →
@@ -177,7 +176,7 @@ instance : AlgebraTower (BTField) where
     exact CommMonoid.mul_comm ((towerAlgebraMap i j h) r) x
   coherence' := by exact fun i j k h1 h2 ↦ towerAlgebraMap_assoc k j i h1 h2
 
-def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) := by
+@[reducible] def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) := by
   exact AlgebraTower.toAlgebra h_le
 
 lemma binaryTowerAlgebra_def (l r : ℕ) (h_le : l ≤ r) :
@@ -213,7 +212,7 @@ theorem binaryTowerAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid : l ≤ mid)
     (h_l_le_mid:=h_l_le_mid) (h_mid_le_r:=h_mid_le_r)]
 
 /-- This also provides the corresponding Module instance. -/
-def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) :=
+@[reducible] def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) :=
   (binaryAlgebraTower (h_le:=h_le)).toModule
 
 instance (priority := 1000) algebra_adjacent_tower (l : ℕ) :