Merge commit '5212dc478426d5caca02fc5aea6df6d211fbdd7e' into bump/nightly-2026-04-06

Author: mathlib4-bot

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean

@@ -48,12 +48,22 @@ public lemma convexOn_ringInverse :
     by_cases ha' : a = 0
     · have hb' : b = 1 := by grind
       simp only [ha', hb', one_mul, zero_add, gt_iff_lt]
-      grind
+      #adaptation_note /-- Before nightly-2026-06-04, this was just `grind.
+      `spectrum_pos` is not activating in `grind` despite the
+      ```
+      grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a
+      ```
+      rule, because `grind` will not fill in the `𝕜 := ℝ`. -/
+      exact zpos.spectrum_pos hr
     · grind [add_pos_of_pos_of_nonneg, mul_nonneg]
   have h₂ : (a • 1 + b • z ^ (-1 : ℝ)) = cfc (fun r => (a + b * r ^ (-1 : ℝ))) z := by
     rw [CFC.rpow_eq_cfc_real zpos.nonneg]
     have hcont : ContinuousOn (fun r : ℝ => (r ^ (-1 : ℝ))) (spectrum ℝ z) :=
-      ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind)
+      ContinuousOn.rpow_const (f := id) (by fun_prop) (by
+        #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
+        intro x h
+        have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
+        grind)
     rw [← cfc_smul b _ z hcont, ← Algebra.algebraMap_eq_smul_one, ← cfc_const_add a _ z]
     refine cfc_congr fun r hr => ?_
     simp
@@ -72,7 +82,11 @@ public lemma convexOn_ringInverse :
           have : 0 ≤ b * r := by positivity
           cases lt_or_eq_of_le ha <;> grind
         · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
-          exact ContinuousOn.rpow_const (by fun_prop) (by grind)
+          exact ContinuousOn.rpow_const (by fun_prop) (by
+            #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
+            intro x h
+            have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
+            grind)
         · intro r hr
           suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
             simp_rw [← Real.rpow_intCast] at this

Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean

@@ -64,9 +64,20 @@ private theorem nthRoot.lt_pow_go_succ_aux0 (hb : b ≠ 0) :
   rw [Nat.le_div_iff_mul_le (by positivity), Nat.mul_comm,
     ← Nat.add_mul_div_right _ _ (by positivity),
     Nat.le_div_iff_mul_le (by positivity)]
+  #adaptation_note /-- Prior to nightly-2026-04-06, this was
+  ```
   have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg
     (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1)
   grind
+  ```
+  -/
+  zify
+  have h := pow_add_mul_le_add_pow_of_sq_nonneg (a := (b : ℤ)) (b := (a : ℤ) - b)
+    (ha := by positivity) (Hsq := by positivity) (Hsq' := by positivity) (H := by omega)
+    (n := n + 1)
+  rw [← sub_nonneg] at h ⊢
+  convert h using 1
+  rw [pow_succ]; push_cast; ring1
 
 private theorem nthRoot.always_exists (n a : ℕ) :
     ∃ c, c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1) := by

Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

@@ -44,7 +44,15 @@ theorem eval_T_real_mem_Icc (n : ℤ) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) :
   grind [T_real_cos, cos_mem_Icc]
 
 theorem abs_eval_T_real_le_one (n : ℤ) {x : ℝ} (hx : |x| ≤ 1) :
-    |(T ℝ n).eval x| ≤ 1 := by grind [eval_T_real_mem_Icc]
+    |(T ℝ n).eval x| ≤ 1 := by
+  #adaptation_note /-- Before nightly-2026-04-07, this was just
+  `grind [eval_T_real_mem_Icc]`. `grind`'s e-matching now keeps the
+  `Polynomial.eval` produced by the lemma (which uses `instCommSemiring.toSemiring`)
+  and the `Polynomial.eval` propagated by abs unfolding (which uses `Real.semiring`)
+  as distinct atoms, even though they are `rfl`-equal, so the contradiction is
+  never found. -/
+  have h := eval_T_real_mem_Icc n (Set.mem_Icc.mpr (abs_le.mp hx))
+  exact abs_le.mpr (Set.mem_Icc.mp h)
 
 theorem one_le_eval_T_real (n : ℤ) {x : ℝ} (hx : 1 ≤ x) : 1 ≤ (T ℝ n).eval x := by
   rw [← cosh_arcosh hx]

Mathlib/Computability/Partrec.lean

@@ -718,9 +718,6 @@ theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
       b ∈ PFun.fix f a := by
   intro F; refine ⟨fun h => ?_, fun h => ?_⟩
   · rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩
-    #adaptation_note /-- Before leanprover/lean4#13166, the proof from here to the end of the
-    first branch was:
-    ```
     have : ∀ m a', Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a := by
       intro m a' am ba
       induction m generalizing a' with simp [F] at am
@@ -754,9 +751,9 @@ theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
       · simpa [F] using Or.inr ⟨_, hk, h₂⟩
       · rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
     · rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
-      #adaptation_note /-- After leanprover/lean4#13166 which arrived in nightly-2026-03-28:
-      This `clear_value` used to not be necessary.
-      -/
+      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
+      (replacing grind's canonicalizer with a type-directed normalizer),
+      the `clear_value F` was not required here. -/
       clear_value F
       grind
 

Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Transform.lean

@@ -136,7 +136,7 @@ lemma G2_eq_tsum_G2Term (z : ℍ) : G2 z = ∑' m, ∑' n, G2Term z ![m, n] := b
       exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])
     · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
         using (G2Term_prod_summable z).prod
-  · grind [(G2Term_prod_summable z).prod.congr]
+  · exact (G2Term_prod_summable z).prod
   · exact summable_zero.congr
       fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]
 

Mathlib/NumberTheory/Padics/MahlerBasis.lean

@@ -176,12 +176,12 @@ private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ}
     refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])
     -- remains to show norm of binomial coeff is `≤ p⁻¹`
     rw [mem_range] at hi
-    have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by lia)
+    have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega)
     rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, PadicInt.norm_eq_zpow_neg_valuation
       (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast,
       zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff,
       ← PadicInt.valuation_coe, PadicInt.coe_natCast, Padic.valuation_natCast, Nat.one_le_cast]
-    exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by lia)
+    exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by omega)
   · -- Bounding the sum over `range (n + 1)`: every term is small by the choice of `t`
     refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_add_one (fun i _ ↦ ?_)
     calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖

Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

@@ -60,7 +60,9 @@ def residueFieldMapCAlgEquiv [J.LiesOver I] (hJ : J = I.map C) :
       apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr
       simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using hr
     refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_
-    simp only [← algebraMap_eq, ← Algebra.smul_def, algebraMap_smul, ← hr]
+    simp only [← algebraMap_eq, ← Algebra.smul_def]
+    erw [algebraMap_smul]
+    simp only [← hr]
     simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using hJ.le hx
   · apply AlgHom.coe_ringHom_injective
     apply IsFractionRing.injective_comp_algebraMap (A := I.ResidueField[X])

Mathlib/RingTheory/Smooth/Local.lean

@@ -86,7 +86,14 @@ theorem FormallySmooth.iff_injective_cotangentComplexBaseChange
       (cotangentComplexBaseChange R S P (ResidueField S)).baseChange K ∘ₗ
       (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.toLinearMap =
       (cotangentComplexBaseChange R S P K) := by
-    ext; simp [cotangentComplexBaseChange_tmul]
+    ext
+    #adaptation_note /-- Prior to nightly-2026-04-06, this was just `simp`. -/
+    simp_rw [AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_comp, curry_apply,
+      LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, Function.comp_apply,
+      AlgebraTensorModule.cancelBaseChange_symm_tmul, LinearMap.baseChange_tmul,
+      cotangentComplexBaseChange_tmul, kerToTensor_apply, one_smul]
+    erw [AlgebraTensorModule.cancelBaseChange_tmul]
+    simp
   rw [← this]
   refine .trans ?_ ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).comp_injective _).symm
   exact ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.injective_comp _).symm

Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

@@ -363,6 +363,8 @@ lemma rankAtStalk_eq (p : PrimeSpectrum R) :
   let e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k]
       k ⊗[R] M :=
     AlgebraTensorModule.cancelBaseChange _ _ _ _ _
-  rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]
+  rw [← e.finrank_eq]
+  erw [finrank_baseChange]
+  rw [rankAtStalk_eq_finrank_tensorProduct]
 
 end Module

Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean

@@ -45,13 +45,16 @@ lemma isNilpotent_tensor_residueField_iff
   · have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial
     simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]
   have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by
-    rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
+    rw [Module.finrank_tensorProduct]
+    erw [Module.finrank_self]
+    rw [one_mul]
   rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]
   simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
     Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul]
   rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)),
     LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange]
-  simp_rw [this, ← ((LinearMap.mul R A) f).charpoly_natDegree]
+  erw [this]
+  simp_rw [← ((LinearMap.mul R A) f).charpoly_natDegree]
   constructor
   · intro e i hi
     replace e := congr(($e).coeff i)
@@ -137,6 +140,7 @@ end PrimeSpectrum
 
 namespace Polynomial
 
+set_option backward.isDefEq.respectTransparency false in
 lemma mem_image_comap_C_basicOpen (f : R[X]) (x : PrimeSpectrum R) :
     x ∈ comap C '' basicOpen f ↔ ∃ i, f.coeff i ∉ x.asIdeal := by
   trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0