Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -338,6 +338,8 @@ theorem mod_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a)
 theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=
   divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot
 
+alias ⟨_, IsRoot.mul_div_eq⟩ := mul_div_eq_iff_isRoot
+
 instance instEuclideanDomain : EuclideanDomain R[X] :=
   { Polynomial.commRing,
     Polynomial.nontrivial with

Mathlib/RingTheory/AdjoinRoot.lean

@@ -401,7 +401,7 @@ variable (f)
 
 theorem mul_div_root_cancel [Fact (Irreducible f)] :
     (X - C (root f)) * ((f.map (of f)) / (X - C (root f))) = f.map (of f) :=
-  mul_div_eq_iff_isRoot.2 <| isRoot_root _
+  (isRoot_root _).mul_div_eq
 
 end Irreducible
 

Mathlib/Tactic/NormNum/Pow.lean

@@ -59,24 +59,25 @@ so we use an additional trick to do binary subdivision on `log2 b`. As a result
 a proof of depth `log (log b)` which will essentially never overflow before the numbers involved
 themselves exceed memory limits.
 -/
-partial def evalNatPow (a b : Q(ℕ)) : (c : Q(ℕ)) × Q(Nat.pow $a $b = $c) :=
+partial def evalNatPow (a b : Q(ℕ)) : OptionT CoreM ((c : Q(ℕ)) × Q(Nat.pow $a $b = $c)) := do
   if b.natLit! = 0 then
     haveI : $b =Q 0 := ⟨⟩
-    ⟨q(nat_lit 1), q(natPow_zero)⟩
+    return ⟨q(nat_lit 1), q(natPow_zero)⟩
   else if a.natLit! = 0 then
     haveI : $a =Q 0 := ⟨⟩
     have b' : Q(ℕ) := mkRawNatLit (b.natLit! - 1)
     haveI : $b =Q Nat.succ $b' := ⟨⟩
-    ⟨q(nat_lit 0), q(zero_natPow)⟩
+    return ⟨q(nat_lit 0), q(zero_natPow)⟩
   else if a.natLit! = 1 then
     haveI : $a =Q 1 := ⟨⟩
-    ⟨q(nat_lit 1), q(one_natPow)⟩
+    return ⟨q(nat_lit 1), q(one_natPow)⟩
   else if b.natLit! = 1 then
     haveI : $b =Q 1 := ⟨⟩
-    ⟨a, q(natPow_one)⟩
+    return ⟨a, q(natPow_one)⟩
   else
+    guard <| ← Lean.checkExponent b.natLit!
     let ⟨c, p⟩ := go b.natLit!.log2 a q(nat_lit 1) a b _ .rfl
-    ⟨c, q(($p).run)⟩
+    return ⟨c, q(($p).run)⟩
 where
   /-- Invariants: `a ^ b₀ = c₀`, `depth > 0`, `b >>> depth = b₀`, `p := Nat.pow $a $b₀ = $c₀` -/
   go (depth : Nat) (a b₀ c₀ b : Q(ℕ)) (p : Q(Prop)) (hp : $p =Q (Nat.pow $a $b₀ = $c₀)) :
@@ -120,28 +121,29 @@ theorem intPow_negOfNat_bit1 {b' c' : ℕ} (h1 : Nat.pow a b' = c')
   simp [mul_comm, mul_left_comm]
 
 /-- Evaluates `Int.pow a b = c` where `a` and `b` are raw integer literals. -/
-partial def evalIntPow (za : ℤ) (a : Q(ℤ)) (b : Q(ℕ)) : ℤ × (c : Q(ℤ)) × Q(Int.pow $a $b = $c) :=
+partial def evalIntPow (za : ℤ) (a : Q(ℤ)) (b : Q(ℕ)) :
+    OptionT CoreM (ℤ × (c : Q(ℤ)) × Q(Int.pow $a $b = $c)) := do
   have a' : Q(ℕ) := a.appArg!
   if 0 ≤ za then
-    haveI : $a =Q .ofNat $a' := ⟨⟩
-    let ⟨c, p⟩ := evalNatPow a' b
-    ⟨c.natLit!, q(.ofNat $c), q(intPow_ofNat $p)⟩
+    have : $a =Q .ofNat $a' := ⟨⟩
+    let ⟨c, p⟩ ← evalNatPow a' b
+    return ⟨c.natLit!, q(.ofNat $c), q(intPow_ofNat $p)⟩
   else
-    haveI : $a =Q .negOfNat $a' := ⟨⟩
+    have : $a =Q .negOfNat $a' := ⟨⟩
     let b' := b.natLit!
     have b₀ : Q(ℕ) := mkRawNatLit (b' >>> 1)
-    let ⟨c₀, p⟩ := evalNatPow a' b₀
+    let ⟨c₀, p⟩ := ← evalNatPow a' b₀
     let c' := c₀.natLit!
     if b' &&& 1 == 0 then
       have c : Q(ℕ) := mkRawNatLit (c' * c')
       have pc : Q($c₀ * $c₀ = $c) := (q(Eq.refl $c) : Expr)
       have pb : Q(2 * $b₀ = $b) := (q(Eq.refl $b) : Expr)
-      ⟨c.natLit!, q(.ofNat $c), q(intPow_negOfNat_bit0 $p $pb $pc)⟩
+      return ⟨c.natLit!, q(.ofNat $c), q(intPow_negOfNat_bit0 $p $pb $pc)⟩
     else
       have c : Q(ℕ) := mkRawNatLit (c' * (c' * a'.natLit!))
       have pc : Q($c₀ * ($c₀ * $a') = $c) := (q(Eq.refl $c) : Expr)
       have pb : Q(2 * $b₀ + 1 = $b) := (q(Eq.refl $b) : Expr)
-      ⟨-c.natLit!, q(.negOfNat $c), q(intPow_negOfNat_bit1 $p $pb $pc)⟩
+      return ⟨-c.natLit!, q(.negOfNat $c), q(intPow_negOfNat_bit1 $p $pb $pc)⟩
 
 -- see note [norm_num lemma function equality]
 theorem isNat_pow {α} [Semiring α] : ∀ {f : α → ℕ → α} {a : α} {b a' b' c : ℕ},
@@ -175,30 +177,30 @@ theorem isNNRat_pow {α} [Semiring α] {f : α → ℕ → α} {a : α} {an cn :
 /-- Main part of `evalPow`. -/
 def evalPow.core {u : Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → ℕ → «$α»)) (a : Q(«$α»))
     (b nb : Q(ℕ)) (pb : Q(IsNat «$b» «$nb»)) (sα : Q(Semiring «$α»)) (ra : Result a) :
-    Option (Result e) := do
+    OptionT CoreM (Result e) := do
   haveI' : $e =Q $a ^ $b := ⟨⟩
   haveI' : $f =Q HPow.hPow := ⟨⟩
   match ra with
   | .isBool .. => failure
   | .isNat sα na pa =>
     assumeInstancesCommute
-    have ⟨c, r⟩ := evalNatPow na nb
+    let ⟨c, r⟩ ← evalNatPow na nb
     return .isNat sα c q(isNat_pow (f := $f) (.refl $f) $pa $pb $r)
   | .isNegNat rα .. =>
     assumeInstancesCommute
-    let ⟨za, na, pa⟩ ← ra.toInt rα
-    have ⟨zc, c, r⟩ := evalIntPow za na nb
+    let ⟨za, na, pa⟩ ← OptionT.mk <| pure (ra.toInt rα)
+    let ⟨zc, c, r⟩ ← evalIntPow za na nb
     return .isInt rα c zc q(isInt_pow (f := $f) (.refl $f) $pa $pb $r)
   | .isNNRat dα _qa na da pa =>
     assumeInstancesCommute
-    have ⟨nc, r1⟩ := evalNatPow na nb
-    have ⟨dc, r2⟩ := evalNatPow da nb
+    let ⟨nc, r1⟩ ← evalNatPow na nb
+    let ⟨dc, r2⟩ ← evalNatPow da nb
     let qc := mkRat nc.natLit! dc.natLit!
     return .isNNRat dα qc nc dc q(isNNRat_pow (f := $f) (.refl $f) $pa $pb $r1 $r2)
   | .isNegNNRat dα qa na da pa =>
     assumeInstancesCommute
-    have ⟨zc, nc, r1⟩ := evalIntPow qa.num q(Int.negOfNat $na) nb
-    have ⟨dc, r2⟩ := evalNatPow da nb
+    let ⟨zc, nc, r1⟩ ← evalIntPow qa.num q(Int.negOfNat $na) nb
+    let ⟨dc, r2⟩ ← evalNatPow da nb
     let qc := mkRat zc dc.natLit!
     return .isRat dα qc nc dc q(isRat_pow (f := $f) (.refl $f) $pa $pb $r1 $r2)
 
@@ -214,7 +216,9 @@ def evalPow : NormNumExt where eval {u α} e := do
   guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(HPow.hPow (α := $α))
   haveI' : $e =Q $a ^ $b := ⟨⟩
   haveI' : $f =Q HPow.hPow := ⟨⟩
-  evalPow.core q($e) q($f) q($a) q($b) q($nb) q($pb) q($sα) ra
+  let .some r ←
+    liftM <| OptionT.run (evalPow.core q($e) q($f) q($a) q($b) q($nb) q($pb) q($sα) ra) | failure
+  return r
 
 theorem isNat_zpow_pos {α : Type*} [DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ}
     (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) :

Mathlib/Tactic/Ring/Basic.lean

@@ -890,6 +890,11 @@ theorem mul_pow {ea₁ b c₁ : ℕ} {xa₁ : R}
     (_ : ea₁ * b = c₁) (_ : a₂ ^ b = c₂) : (xa₁ ^ ea₁ * a₂ : R) ^ b = xa₁ ^ c₁ * c₂ := by
   subst_vars; simp [_root_.mul_pow, pow_mul]
 
+-- needed to lift from `OptionT CoreM` to `OptionT MetaM`
+private local instance {m m'} [Monad m] [Monad m'] [MonadLiftT m m'] :
+    MonadLiftT (OptionT m) (OptionT m') where
+  monadLift x := OptionT.mk x.run
+
 /-- There are several special cases when exponentiating monomials:
 
 * `1 ^ n = 1`

Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

@@ -224,7 +224,7 @@ lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X :=
   · intro w
     simp only [U]
     split_ifs with hw
-    · exact Valued.isOpen_closedball _ z0.ne'
+    · exact Valued.isOpen_closedBall _ z0.ne'
     · refine Valued.isOpen_sphere _ ?_
       push_neg at hw
       refine (hw.trans' ?_).ne'

Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

@@ -216,14 +216,17 @@ theorem isClopen_ball (r : Γ₀) : IsClopen (X := R) {x | v x < r} :=
   ⟨isClosed_ball _ _, isOpen_ball _ _⟩
 
 /-- A closed ball centred at the origin in a valued ring is open. -/
-theorem isOpen_closedball {r : Γ₀} (hr : r ≠ 0) : IsOpen (X := R) {x | v x ≤ r} := by
+theorem isOpen_closedBall {r : Γ₀} (hr : r ≠ 0) : IsOpen (X := R) {x | v x ≤ r} := by
   rw [isOpen_iff_mem_nhds]
   intro x hx
   rw [mem_nhds]
   simp only [setOf_subset_setOf]
   exact ⟨Units.mk0 _ hr,
     fun y hy => (sub_add_cancel y x).symm ▸ le_trans (v.map_add _ _) (max_le (le_of_lt hy) hx)⟩
 
+@[deprecated (since := "2025-10-09")]
+alias isOpen_closedball := isOpen_closedBall
+
 /-- A closed ball centred at the origin in a valued ring is closed. -/
 theorem isClosed_closedBall (r : Γ₀) : IsClosed (X := R) {x | v x ≤ r} := by
   rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
@@ -235,7 +238,7 @@ theorem isClosed_closedBall (r : Γ₀) : IsClosed (X := R) {x | v x ≤ r} := b
 
 /-- A closed ball centred at the origin in a valued ring is clopen. -/
 theorem isClopen_closedBall {r : Γ₀} (hr : r ≠ 0) : IsClopen (X := R) {x | v x ≤ r} :=
-  ⟨isClosed_closedBall _ _, isOpen_closedball _ hr⟩
+  ⟨isClosed_closedBall _ _, isOpen_closedBall _ hr⟩
 
 /-- A sphere centred at the origin in a valued ring is clopen. -/
 theorem isClopen_sphere {r : Γ₀} (hr : r ≠ 0) : IsClopen (X := R) {x | v x = r} := by
@@ -257,7 +260,7 @@ theorem isClosed_sphere (r : Γ₀) : IsClosed (X := R) {x | v x = r} := by
 
 /-- The closed unit ball in a valued ring is open. -/
 theorem isOpen_integer : IsOpen (_i.v.integer : Set R) :=
-  isOpen_closedball _ one_ne_zero
+  isOpen_closedBall _ one_ne_zero
 
 @[deprecated (since := "2025-04-25")]
 alias integer_isOpen := isOpen_integer

Mathlib/Topology/ContinuousMap/CompactlySupported.lean

@@ -715,45 +715,10 @@ lemma exists_add_nnrealPart_add_eq (f g : C_c(α, ℝ)) : ∃ (h : C_c(α, ℝ
   use h
   refine ⟨hh, ?_⟩
   ext x
+  have hhx := congr(($hh x : ℝ))
   simp only [coe_add, Pi.add_apply, nnrealPart_apply, coe_neg, Pi.neg_apply, NNReal.coe_add,
-    Real.coe_toNNReal', ← neg_add]
-  have hhx : (f x + g x) ⊔ 0 + ↑(h x) = f x ⊔ 0 + g x ⊔ 0 := by
-    rw [← Real.coe_toNNReal', ← Real.coe_toNNReal', ← Real.coe_toNNReal', ← NNReal.coe_add,
-      ← NNReal.coe_add]
-    have hhx' : ((f + g).nnrealPart + h) x = (f.nnrealPart + g.nnrealPart) x := by congr
-    simp only [coe_add, Pi.add_apply, nnrealPart_apply] at hhx'
-    exact congrArg toReal hhx'
-  rcases le_total 0 (f x) with hfx | hfx
-  · rcases le_total 0 (g x) with hgx | hgx
-    · simp only [hfx, hgx, add_nonneg, sup_of_le_left, add_eq_left, coe_eq_zero] at hhx
-      simp [hhx, hfx, hgx, add_nonpos]
-    · rcases le_total 0 (f x + g x) with hfgx | hfgx
-      · simp only [hfgx, sup_of_le_left, add_assoc, hfx, hgx, sup_of_le_right, add_zero,
-        add_eq_left] at hhx
-        rw [sup_of_le_right (neg_nonpos.mpr hfx), sup_of_le_left (neg_nonneg.mpr hgx),
-          sup_of_le_right (neg_nonpos.mpr hfgx)]
-        linarith
-      · simp only [hfgx, sup_of_le_right, zero_add, hfx, sup_of_le_left, hgx, add_zero] at hhx
-        rw [sup_of_le_right (neg_nonpos.mpr hfx), sup_of_le_left (neg_nonneg.mpr hgx),
-          sup_of_le_left (neg_nonneg.mpr hfgx), hhx]
-        ring
-  · rcases le_total 0 (g x) with hgx | hgx
-    · rcases le_total 0 (f x + g x) with hfgx | hfgx
-      · simp only [hfgx, sup_of_le_left, add_comm, hfx, sup_of_le_right, hgx, zero_add] at hhx
-        rw [sup_of_le_left (neg_nonneg.mpr hfx), sup_of_le_right (neg_nonpos.mpr hgx),
-          sup_of_le_right (neg_nonpos.mpr hfgx), zero_add, add_zero]
-        linarith
-      · simp only [hfgx, sup_of_le_right, zero_add, hfx, hgx, sup_of_le_left] at hhx
-        rw [sup_of_le_left (neg_nonneg.mpr hfx), sup_of_le_right (neg_nonpos.mpr hgx),
-          sup_of_le_left (neg_nonneg.mpr hfgx), hhx]
-        ring
-    · simp only [(add_nonpos hfx hgx), sup_of_le_right, zero_add, hfx, hgx, add_zero,
-        coe_eq_zero] at hhx
-      rw [sup_of_le_left (neg_nonneg.mpr hfx),
-        sup_of_le_left (neg_nonneg.mpr hgx),
-        sup_of_le_left (neg_nonneg.mpr (add_nonpos hfx hgx)), hhx, neg_add_rev, NNReal.coe_zero,
-        add_zero]
-      ring
+    Real.coe_toNNReal', ← neg_add, max_neg_zero] at hhx ⊢
+  linear_combination hhx
 
 /-- The compactly supported continuous `ℝ≥0`-valued function as a compactly supported `ℝ`-valued
 function. -/

MathlibTest/norm_num.lean

@@ -751,3 +751,9 @@ example : (1 : R PUnit.{u+1} PUnit.{v+1}) <= 2 := by
 -- asymptotically slower than the GMP implementation.
 -- It would be great to fix that, and restore this test.
 example : 10^400000 = 10^400000 := by norm_num
+
+theorem large1 {α} [Ring α] : 2^(2^2000) + (2*2) - 2^(2^2000) = (4 : α) := by
+  -- large powers ignored rather than hanging
+  set_option exponentiation.threshold 20 in
+    norm_num1 -- TODO: this should warn, but the warning is discarded
+  simp only [add_sub_cancel_left]

MathlibTest/norm_num_ext.lean

@@ -27,6 +27,9 @@ import Mathlib.Tactic.Simproc.Factors
 Some tests of unported extensions are still commented out.
 -/
 
+-- The default is very low, and we want to test performance on large numbers.
+set_option exponentiation.threshold 2000
+
 -- set_option profiler true
 -- set_option trace.profiler true
 -- set_option trace.Tactic.norm_num true