bump to nightly-2023-03-08-12

mathlib commit leanprover-community/mathlib@38f16f9

Mathbin/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -690,7 +690,7 @@ noncomputable def xClass : W.CoordinateRing :=
 #align weierstrass_curve.coordinate_ring.X_class WeierstrassCurve.CoordinateRing.xClass
 
 theorem xClass_ne_zero [Nontrivial R] : xClass W x ≠ 0 :=
-  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (C_ne_zero.mpr <| x_sub_c_ne_zero x) <|
+  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (C_ne_zero.mpr <| X_sub_C_ne_zero x) <|
     by
     rw [nat_degree_polynomial, nat_degree_C]
     norm_num1
@@ -703,7 +703,7 @@ noncomputable def yClass : W.CoordinateRing :=
 #align weierstrass_curve.coordinate_ring.Y_class WeierstrassCurve.CoordinateRing.yClass
 
 theorem yClass_ne_zero [Nontrivial R] : yClass W y ≠ 0 :=
-  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (x_sub_c_ne_zero y) <|
+  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (X_sub_C_ne_zero y) <|
     by
     rw [nat_degree_polynomial, nat_degree_X_sub_C]
     norm_num1

Mathbin/Data/Polynomial/Derivative.lean

@@ -243,7 +243,7 @@ theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) :
 
 @[simp]
 theorem iterate_derivative_c {k} (h : 0 < k) : (derivative^[k]) (C a : R[X]) = 0 :=
-  iterate_derivative_eq_zero <| (natDegree_c _).trans_lt h
+  iterate_derivative_eq_zero <| (natDegree_C _).trans_lt h
 #align polynomial.iterate_derivative_C Polynomial.iterate_derivative_c
 
 @[simp]
@@ -253,7 +253,7 @@ theorem iterate_derivative_one {k} (h : 0 < k) : (derivative^[k]) (1 : R[X]) = 0
 
 @[simp]
 theorem iterate_derivative_x {k} (h : 1 < k) : (derivative^[k]) (X : R[X]) = 0 :=
-  iterate_derivative_eq_zero <| natDegree_x_le.trans_lt h
+  iterate_derivative_eq_zero <| natDegree_X_le.trans_lt h
 #align polynomial.iterate_derivative_X Polynomial.iterate_derivative_x
 
 theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]}
@@ -276,7 +276,7 @@ theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f :
 
 theorem eq_c_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]} (h : f.derivative = 0) :
     f = C (f.coeff 0) :=
-  eq_c_of_natDegree_eq_zero <| natDegree_eq_zero_of_derivative_eq_zero h
+  eq_C_of_natDegree_eq_zero <| natDegree_eq_zero_of_derivative_eq_zero h
 #align polynomial.eq_C_of_derivative_eq_zero Polynomial.eq_c_of_derivative_eq_zero
 
 @[simp]

Mathbin/Data/Polynomial/FieldDivision.lean

@@ -507,7 +507,7 @@ theorem not_irreducible_c (x : R) : ¬Irreducible (C x) :=
 
 theorem degree_pos_of_irreducible (hp : Irreducible p) : 0 < p.degree :=
   lt_of_not_ge fun hp0 =>
-    have := eq_c_of_degree_le_zero hp0
+    have := eq_C_of_degree_le_zero hp0
     not_irreducible_c (p.coeff 0) <| this ▸ hp
 #align polynomial.degree_pos_of_irreducible Polynomial.degree_pos_of_irreducible
 
@@ -520,7 +520,7 @@ theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type _} [Field K] (
   refine'
     Or.resolve_left
       (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
-        (irreducible_of_degree_eq_one (Polynomial.degree_x_sub_c a)))
+        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a)))
       _
   contrapose! hf' with h
   have key : (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a) :=

Mathbin/Data/Polynomial/Inductions.lean

@@ -145,7 +145,7 @@ theorem degree_pos_induction_on {P : R[X] → Prop} (p : R[X]) (h0 : 0 < degree
     (fun p a _ _ ih h0 =>
       have : 0 < degree p :=
         lt_of_not_ge fun h =>
-          not_lt_of_ge degree_c_le <| by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0
+          not_lt_of_ge degree_C_le <| by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0
       hadd this (ih this))
     (fun p _ ih h0' =>
       if h0 : 0 < degree p then hX h0 (ih h0)

Mathbin/Data/Polynomial/Monic.lean

@@ -101,12 +101,12 @@ theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1)
 theorem monic_x_pow_add {n : ℕ} (H : degree p ≤ n) : Monic (X ^ (n + 1) + p) :=
   have H1 : degree p < n + 1 := lt_of_le_of_lt H (WithBot.coe_lt_coe.2 (Nat.lt_succ_self n))
   monic_of_degree_le (n + 1)
-    (le_trans (degree_add_le _ _) (max_le (degree_x_pow_le _) (le_of_lt H1)))
+    (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H1)))
     (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero])
 #align polynomial.monic_X_pow_add Polynomial.monic_x_pow_add
 
 theorem monic_x_add_c (x : R) : Monic (X + C x) :=
-  pow_one (X : R[X]) ▸ monic_x_pow_add degree_c_le
+  pow_one (X : R[X]) ▸ monic_x_pow_add degree_C_le
 #align polynomial.monic_X_add_C Polynomial.monic_x_add_c
 
 theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=

Mathbin/Data/Polynomial/RingDivision.lean

@@ -236,7 +236,7 @@ theorem degree_coe_units [Nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0 :=
 theorem isUnit_iff : IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
   ⟨fun hp =>
     ⟨p.coeff 0,
-      let h := eq_c_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
+      let h := eq_C_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
       ⟨isUnit_C.1 (h ▸ hp), h.symm⟩⟩,
     fun ⟨r, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩
 #align polynomial.is_unit_iff Polynomial.isUnit_iff
@@ -246,7 +246,7 @@ variable [CharZero R]
 @[simp]
 theorem degree_bit0_eq (p : R[X]) : degree (bit0 p) = degree p := by
   rw [bit0_eq_two_mul, degree_mul, (by simp : (2 : R[X]) = C 2),
-    @Polynomial.degree_c R _ _ two_ne_zero, zero_add]
+    @Polynomial.degree_C R _ _ two_ne_zero, zero_add]
 #align polynomial.degree_bit0_eq Polynomial.degree_bit0_eq
 
 @[simp]
@@ -405,7 +405,7 @@ section Roots
 open Multiset
 
 theorem prime_x_sub_c (r : R) : Prime (X - C r) :=
-  ⟨x_sub_c_ne_zero r, not_isUnit_x_sub_c r, fun _ _ =>
+  ⟨X_sub_C_ne_zero r, not_isUnit_x_sub_c r, fun _ _ =>
     by
     simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero]
     exact id⟩
@@ -550,7 +550,7 @@ theorem card_roots_sub_c {p : R[X]} {a : R} (hp0 : 0 < degree p) :
     ((p - C a).roots.card : WithBot ℕ) ≤ degree p :=
   calc
     ((p - C a).roots.card : WithBot ℕ) ≤ degree (p - C a) :=
-      card_roots <| mt sub_eq_zero.1 fun h => not_le_of_gt hp0 <| h.symm ▸ degree_c_le
+      card_roots <| mt sub_eq_zero.1 fun h => not_le_of_gt hp0 <| h.symm ▸ degree_C_le
     _ = degree p := by rw [sub_eq_add_neg, ← C_neg] <;> exact degree_add_C hp0
 
 #align polynomial.card_roots_sub_C Polynomial.card_roots_sub_c
@@ -633,7 +633,7 @@ theorem mem_roots_sub_C' {p : R[X]} {a x : R} : x ∈ (p - C a).roots ↔ p ≠
 
 theorem mem_roots_sub_c {p : R[X]} {a x : R} (hp0 : 0 < degree p) :
     x ∈ (p - C a).roots ↔ p.eval x = a :=
-  mem_roots_sub_C'.trans <| and_iff_right fun hp => hp0.not_le <| hp.symm ▸ degree_c_le
+  mem_roots_sub_C'.trans <| and_iff_right fun hp => hp0.not_le <| hp.symm ▸ degree_C_le
 #align polynomial.mem_roots_sub_C Polynomial.mem_roots_sub_c
 
 @[simp]
@@ -719,7 +719,7 @@ theorem roots_monomial (ha : a ≠ 0) (n : ℕ) : (monomial n a).roots = n • {
 #align polynomial.roots_monomial Polynomial.roots_monomial
 
 theorem roots_prod_x_sub_c (s : Finset R) : (s.Prod fun a => X - C a).roots = s.val :=
-  (roots_prod (fun a => X - C a) s (prod_ne_zero_iff.mpr fun a _ => x_sub_c_ne_zero a)).trans
+  (roots_prod (fun a => X - C a) s (prod_ne_zero_iff.mpr fun a _ => X_sub_C_ne_zero a)).trans
     (by simp_rw [roots_X_sub_C, Multiset.bind_singleton, Multiset.map_id'])
 #align polynomial.roots_prod_X_sub_C Polynomial.roots_prod_x_sub_c
 
@@ -749,8 +749,8 @@ theorem card_roots_x_pow_sub_c {n : ℕ} (hn : 0 < n) (a : R) :
   WithBot.coe_le_coe.1 <|
     calc
       ((roots ((X : R[X]) ^ n - C a)).card : WithBot ℕ) ≤ degree ((X : R[X]) ^ n - C a) :=
-        card_roots (x_pow_sub_c_ne_zero hn a)
-      _ = n := degree_x_pow_sub_c hn a
+        card_roots (X_pow_sub_C_ne_zero hn a)
+      _ = n := degree_X_pow_sub_C hn a
 
 #align polynomial.card_roots_X_pow_sub_C Polynomial.card_roots_x_pow_sub_c
 
@@ -825,7 +825,7 @@ theorem Monic.comp_x_sub_c (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic :=
 #align polynomial.monic.comp_X_sub_C Polynomial.Monic.comp_x_sub_c
 
 theorem units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by
-  rw [← Polynomial.C_mul', ← Polynomial.eq_c_of_degree_eq_zero (degree_coe_units c)]
+  rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
 #align polynomial.units_coeff_zero_smul Polynomial.units_coeff_zero_smul
 
 @[simp]
@@ -984,7 +984,7 @@ theorem degree_eq_one_of_irreducible_of_root (hi : Irreducible p) {x : R} (hx :
   have : IsUnit (X - C x) ∨ IsUnit g := hi.isUnit_or_isUnit hg
   this.elim
     (fun h => by
-      have h₁ : degree (X - C x) = 1 := degree_x_sub_c x
+      have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
       have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
       rw [h₁] at h₂ <;> exact absurd h₂ (by decide))
     fun hgu => by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_is_unit hgu, add_zero]

Mathbin/Data/Polynomial/Splits.lean

@@ -141,11 +141,11 @@ theorem splits_of_isUnit [IsDomain K] {u : K[X]} (hu : IsUnit u) : u.Splits i :=
 #align polynomial.splits_of_is_unit Polynomial.splits_of_isUnit
 
 theorem splits_x_sub_c {x : K} : (X - C x).Splits i :=
-  splits_of_degree_le_one _ <| degree_x_sub_c_le _
+  splits_of_degree_le_one _ <| degree_X_sub_C_le _
 #align polynomial.splits_X_sub_C Polynomial.splits_x_sub_c
 
 theorem splits_x : X.Splits i :=
-  splits_of_degree_le_one _ degree_x_le
+  splits_of_degree_le_one _ degree_X_le
 #align polynomial.splits_X Polynomial.splits_x
 
 theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : Finset ι} :

Mathbin/FieldTheory/Galois.lean

@@ -481,7 +481,7 @@ theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separ
   · have key :=
       IntermediateField.card_algHom_adjoin_integral F
         (show IsIntegral F (0 : E) from isIntegral_zero)
-    rw [minpoly.zero, Polynomial.natDegree_x] at key
+    rw [minpoly.zero, Polynomial.natDegree_X] at key
     specialize key Polynomial.separable_x (Polynomial.splits_x (algebraMap F E))
     rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
     refine' Eq.trans _ key

Mathbin/FieldTheory/Ratfunc.lean

@@ -1072,15 +1072,15 @@ def numDenom (x : Ratfunc K) : K[X] × K[X] :=
       have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq
       have hdeg' : (Polynomial.C a.leading_coeff⁻¹ * gcd p q).degree ≤ q.degree :=
         by
-        rw [Polynomial.degree_mul, Polynomial.degree_c hainv, zero_add]
+        rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]
         exact hdeg
       have hdivp : Polynomial.C a.leading_coeff⁻¹ * gcd p q ∣ p :=
         (C_mul_dvd hainv).mpr (gcd_dvd_left p q)
       have hdivq : Polynomial.C a.leading_coeff⁻¹ * gcd p q ∣ q :=
         (C_mul_dvd hainv).mpr (gcd_dvd_right p q)
       rw [EuclideanDomain.mul_div_mul_cancel ha hdivp, EuclideanDomain.mul_div_mul_cancel ha hdivq,
         leading_coeff_div hdeg, leading_coeff_div hdeg', Polynomial.leadingCoeff_mul,
-        Polynomial.leadingCoeff_c, div_C_mul, div_C_mul, ← mul_assoc, ← Polynomial.C_mul, ←
+        Polynomial.leadingCoeff_C, div_C_mul, div_C_mul, ← mul_assoc, ← Polynomial.C_mul, ←
         mul_assoc, ← Polynomial.C_mul]
       constructor <;> congr <;>
         rw [inv_div, mul_comm, mul_div_assoc, ← mul_assoc, inv_inv, _root_.mul_inv_cancel ha',
@@ -1541,7 +1541,7 @@ theorem intDegree_c (k : K) : intDegree (Ratfunc.c k) = 0 := by
 
 @[simp]
 theorem intDegree_x : intDegree (x : Ratfunc K) = 1 := by
-  rw [int_degree, Ratfunc.num_x, Polynomial.natDegree_x, Ratfunc.denom_x, Polynomial.natDegree_one,
+  rw [int_degree, Ratfunc.num_x, Polynomial.natDegree_X, Ratfunc.denom_x, Polynomial.natDegree_one,
     Int.ofNat_one, Int.ofNat_zero, sub_zero]
 #align ratfunc.int_degree_X Ratfunc.intDegree_x
 

Mathbin/LinearAlgebra/Eigenspace.lean

@@ -154,7 +154,7 @@ theorem eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : K[X]) (hq : degr
 theorem ker_aeval_ring_hom'_unit_polynomial (f : End K V) (c : K[X]ˣ) :
     (aeval f (c : K[X])).ker = ⊥ :=
   by
-  rw [Polynomial.eq_c_of_degree_eq_zero (degree_coe_units c)]
+  rw [Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
   simp only [aeval_def, eval₂_C]
   apply ker_algebra_map_End
   apply coeff_coe_units_zero_ne_zero c

Mathbin/RingTheory/Algebraic.lean

@@ -110,7 +110,7 @@ theorem isAlgebraic_zero [Nontrivial R] : IsAlgebraic R (0 : A) :=
 
 /-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
 theorem isAlgebraic_algebraMap [Nontrivial R] (x : R) : IsAlgebraic R (algebraMap R A x) :=
-  ⟨_, x_sub_c_ne_zero x, by rw [_root_.map_sub, aeval_X, aeval_C, sub_self]⟩
+  ⟨_, X_sub_C_ne_zero x, by rw [_root_.map_sub, aeval_X, aeval_C, sub_self]⟩
 #align is_algebraic_algebra_map isAlgebraic_algebraMap
 
 theorem isAlgebraic_one [Nontrivial R] : IsAlgebraic R (1 : A) :=

Mathbin/RingTheory/IsAdjoinRoot.lean

@@ -254,7 +254,7 @@ theorem lift_algebraMap (h : IsAdjoinRoot S f) (a : R) : h.lift i x hx (algebraM
 theorem apply_eq_lift (h : IsAdjoinRoot S f) (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a)
     (hroot : g h.root = x) (a : S) : g a = h.lift i x hx a :=
   by
-  rw [← h.map_repr a, Polynomial.as_sum_range_c_mul_x_pow (h.repr a)]
+  rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]
   simp only [map_sum, map_mul, map_pow, h.map_X, hroot, ← h.algebra_map_apply, hmap, lift_root,
     lift_algebra_map]
 #align is_adjoin_root.apply_eq_lift IsAdjoinRoot.apply_eq_lift

Mathbin/RingTheory/Localization/Integral.lean

@@ -291,7 +291,7 @@ theorem IsIntegral.exists_multiple_integral_of_isLocalization [Algebra Rₘ S] [
   by
   cases' subsingleton_or_nontrivial Rₘ with _ nontriv <;> skip
   · haveI := (algebraMap Rₘ S).codomain_trivial
-    exact ⟨1, Polynomial.X, Polynomial.monic_x, Subsingleton.elim _ _⟩
+    exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
   obtain ⟨p, hp₁, hp₂⟩ := hx
   obtain ⟨p', hp'₁, -, hp'₂⟩ :=
     lifts_and_nat_degree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p _) _

Mathbin/RingTheory/Polynomial/Basic.lean

@@ -611,7 +611,7 @@ theorem mem_leadingCoeffNth_zero (x) : x ∈ I.leadingCoeffNth 0 ↔ C x ∈ I :
     ⟨fun ⟨p, hpI, hpdeg, hpx⟩ => by
       rwa [← hpx, Polynomial.leadingCoeff,
         Nat.eq_zero_of_le_zero (nat_degree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg],
-      fun hx => ⟨C x, hx, degree_c_le, leadingCoeff_c x⟩⟩
+      fun hx => ⟨C x, hx, degree_C_le, leadingCoeff_C x⟩⟩
 #align ideal.mem_leading_coeff_nth_zero Ideal.mem_leadingCoeffNth_zero
 
 theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n :=
@@ -944,7 +944,7 @@ instance (priority := 100) {R : Type _} [CommRing R] [IsDomain R] [WfDvdMonoid R
       · simp only [hdeg, add_zero]
         refine' Prod.Lex.right _ ⟨_, ⟨c.leading_coeff, fun unit_c => not_unit_c _, rfl⟩⟩
         · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
-        rw [Polynomial.isUnit_iff, Polynomial.eq_c_of_degree_eq_zero hdeg]
+        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
         use c.leading_coeff, unit_c
         rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
       · apply Prod.Lex.left
@@ -1021,14 +1021,14 @@ protected theorem Polynomial.isNoetherianRing [IsNoetherianRing R] : IsNoetheria
               exact hp0 H
             have h1 : p.degree = (q * Polynomial.X ^ (k - q.nat_degree)).degree :=
               by
-              rw [Polynomial.degree_mul', Polynomial.degree_x_pow]
+              rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
               rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
               rw [← WithBot.coe_add, add_tsub_cancel_of_le, hn]
               · refine' le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
-              rw [Polynomial.leadingCoeff_x_pow, mul_one]
+              rw [Polynomial.leadingCoeff_X_pow, mul_one]
               exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
             have h2 : p.leading_coeff = (q * Polynomial.X ^ (k - q.nat_degree)).leadingCoeff := by
-              rw [← hlqp, Polynomial.leadingCoeff_mul_x_pow]
+              rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
             have := Polynomial.degree_sub_lt h1 hp0 h2
             rw [Polynomial.degree_eq_natDegree hp0] at this
             rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.nat_degree))]

Mathbin/Tactic/ComputeDegree.lean

@@ -144,16 +144,16 @@ open Expr Polynomial
                             ( add_le_add _ _ ) . trans ( _ : $ ( d1 ) + $ ( d2 ) ≤ $ ( tr ) )
                           )
               | q( - $ ( f ) ) => refine ` `( ( natDegree_neg _ ) . le . trans _ )
-              | q( X ^ $ ( n ) ) => refine ` `( ( natDegree_x_pow_le $ ( n ) ) . trans _ )
+              | q( X ^ $ ( n ) ) => refine ` `( ( natDegree_X_pow_le $ ( n ) ) . trans _ )
               |
                 app q( ⇑ ( @ monomial $ ( R ) $ ( inst ) $ ( n ) ) ) x
                 =>
                 refine ` `( ( natDegree_monomial_le $ ( x ) ) . trans _ )
               |
                 app q( ⇑ C ) x
                 =>
-                refine ` `( ( natDegree_c $ ( x ) ) . le . trans ( Nat.zero_le $ ( tr ) ) )
-              | q( X ) => refine ` `( natDegree_x_le . trans _ )
+                refine ` `( ( natDegree_C $ ( x ) ) . le . trans ( Nat.zero_le $ ( tr ) ) )
+              | q( X ) => refine ` `( natDegree_X_le . trans _ )
               | q( Zero.zero ) => refine ` `( natDegree_zero . le . trans ( Nat.zero_le _ ) )
               | q( One.one ) => refine ` `( natDegree_one . le . trans ( Nat.zero_le _ ) )
               | q( bit0 $ ( a ) ) => refine ` `( ( natDegree_bit0 $ ( a ) ) . trans _ )

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "a577a6450914db668f5c3922c315203f4b3b9bdc",
+    "rev": "ced9d32fdba1f262d9d35520228780f74c2a942c",
     "name": "lean3port",
-    "inputRev?": "a577a6450914db668f5c3922c315203f4b3b9bdc"}},
+    "inputRev?": "ced9d32fdba1f262d9d35520228780f74c2a942c"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "d0620ef77f13b16dd8ba0b52f6ef2301e8caff2c",
+    "rev": "d46c392ec09ae88c092b477f6fc036d3ab96284b",
     "name": "mathlib",
-    "inputRev?": "d0620ef77f13b16dd8ba0b52f6ef2301e8caff2c"}},
+    "inputRev?": "d46c392ec09ae88c092b477f6fc036d3ab96284b"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-08-10"
+def tag : String := "nightly-2023-03-08-12"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a577a6450914db668f5c3922c315203f4b3b9bdc"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ced9d32fdba1f262d9d35520228780f74c2a942c"
 
 @[default_target]
 lean_lib Mathbin where