From 55190306902994d8dd434be9a300cdc8fdc11872 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 9 Nov 2023 03:33:42 +0000 Subject: [PATCH 01/10] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/2778 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 01abdae87ef74..8070bf4b3cb3b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-11-08 +leanprover/lean4-pr-releases:pr-release-2778 From 1aadd4f4012334f6f1cd811e685b9c75a27ee9ed Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 27 Oct 2023 18:40:22 -0700 Subject: [PATCH 02/10] remove macro_rules --- Archive/Imo/Imo1962Q4.lean | 2 -- Archive/Imo/Imo2001Q2.lean | 2 -- Archive/Imo/Imo2008Q3.lean | 2 -- Archive/Imo/Imo2013Q5.lean | 2 -- Archive/Imo/Imo2019Q4.lean | 2 -- Archive/Wiedijk100Theorems/AbelRuffini.lean | 2 -- Archive/Wiedijk100Theorems/AreaOfACircle.lean | 3 --- Archive/Wiedijk100Theorems/HeronsFormula.lean | 2 -- Mathlib/Analysis/Analytic/RadiusLiminf.lean | 2 -- Mathlib/Analysis/BoxIntegral/Basic.lean | 2 -- Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean | 2 -- Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean | 2 -- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean | 2 -- Mathlib/Analysis/Calculus/Monotone.lean | 2 -- Mathlib/Analysis/Complex/Liouville.lean | 3 --- Mathlib/Analysis/Complex/LocallyUniformLimit.lean | 2 -- Mathlib/Analysis/Complex/PhragmenLindelof.lean | 1 - Mathlib/Analysis/Complex/RemovableSingularity.lean | 2 -- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean | 3 --- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean | 2 -- Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean | 2 -- Mathlib/Analysis/Convex/Strong.lean | 2 -- Mathlib/Analysis/Distribution/SchwartzSpace.lean | 2 -- Mathlib/Analysis/Fourier/AddCircle.lean | 2 -- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean | 2 -- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 2 -- Mathlib/Analysis/InnerProductSpace/Calculus.lean | 2 -- Mathlib/Analysis/InnerProductSpace/PiL2.lean | 2 -- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean | 2 -- Mathlib/Analysis/InnerProductSpace/Spectrum.lean | 2 -- Mathlib/Analysis/InnerProductSpace/TwoDim.lean | 2 -- Mathlib/Analysis/InnerProductSpace/l2Space.lean | 2 -- Mathlib/Analysis/Matrix.lean | 3 --- Mathlib/Analysis/MeanInequalities.lean | 2 -- Mathlib/Analysis/MeanInequalitiesPow.lean | 2 -- Mathlib/Analysis/NormedSpace/PiLp.lean | 2 -- Mathlib/Analysis/NormedSpace/ProdLp.lean | 2 -- Mathlib/Analysis/NormedSpace/QuaternionExponential.lean | 2 -- Mathlib/Analysis/NormedSpace/Star/Matrix.lean | 2 -- Mathlib/Analysis/NormedSpace/lpSpace.lean | 3 --- Mathlib/Analysis/ODE/PicardLindelof.lean | 2 -- Mathlib/Analysis/PSeries.lean | 3 --- Mathlib/Analysis/SpecialFunctions/CompareExp.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Gaussian.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Integrals.lean | 2 -- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean | 1 - Mathlib/Analysis/SpecialFunctions/PolarCoord.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean | 4 ---- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean | 1 - Mathlib/Analysis/SpecialFunctions/Stirling.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean | 2 -- .../Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean | 2 -- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean | 2 -- .../Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean | 2 -- .../SpecialFunctions/Trigonometric/EulerSineProd.lean | 3 --- Mathlib/Analysis/SpecificLimits/FloorPow.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean | 2 -- Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean | 2 -- Mathlib/Data/PNat/Basic.lean | 2 -- Mathlib/Data/Real/Pi/Bounds.lean | 2 -- Mathlib/Data/Real/Pi/Leibniz.lean | 2 -- Mathlib/Data/Real/Pi/Wallis.lean | 2 -- Mathlib/Data/ZMod/IntUnitsPower.lean | 2 -- Mathlib/FieldTheory/AbelRuffini.lean | 2 -- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean | 2 -- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean | 2 -- Mathlib/Geometry/Euclidean/Inversion/Calculus.lean | 2 -- Mathlib/Geometry/Euclidean/Triangle.lean | 2 -- Mathlib/Geometry/Manifold/Instances/Sphere.lean | 2 -- Mathlib/LinearAlgebra/Basic.lean | 2 -- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean | 2 -- Mathlib/MeasureTheory/Covering/Differentiation.lean | 3 --- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean | 2 -- Mathlib/MeasureTheory/Function/Jacobian.lean | 3 --- Mathlib/MeasureTheory/Function/L2Space.lean | 3 --- Mathlib/MeasureTheory/Function/LpSpace.lean | 2 -- Mathlib/MeasureTheory/Integral/CircleIntegral.lean | 2 -- Mathlib/MeasureTheory/Integral/CircleTransform.lean | 2 -- Mathlib/MeasureTheory/Integral/MeanInequalities.lean | 2 -- Mathlib/MeasureTheory/Integral/PeakFunction.lean | 3 --- Mathlib/MeasureTheory/Integral/TorusIntegral.lean | 1 - Mathlib/MeasureTheory/Measure/Doubling.lean | 3 --- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean | 2 -- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean | 2 -- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean | 2 -- Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean | 2 -- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean | 2 -- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean | 2 -- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean | 1 - Mathlib/NumberTheory/Cyclotomic/Rat.lean | 2 -- .../NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean | 2 -- Mathlib/NumberTheory/Liouville/LiouvilleWith.lean | 2 -- Mathlib/NumberTheory/Liouville/Measure.lean | 2 -- Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean | 2 -- Mathlib/NumberTheory/ModularForms/SlashActions.lean | 2 -- Mathlib/NumberTheory/NumberField/Embeddings.lean | 2 -- Mathlib/NumberTheory/SumFourSquares.lean | 2 -- Mathlib/NumberTheory/ZetaFunction.lean | 2 -- Mathlib/NumberTheory/ZetaValues.lean | 2 -- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean | 2 -- Mathlib/Probability/Distributions/Gaussian.lean | 2 -- Mathlib/Probability/StrongLaw.lean | 2 -- Mathlib/Probability/Variance.lean | 2 -- Mathlib/RingTheory/LocalProperties.lean | 2 -- Mathlib/RingTheory/Polynomial/Selmer.lean | 2 -- Mathlib/RingTheory/RootsOfUnity/Basic.lean | 2 -- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean | 2 -- Mathlib/RingTheory/WittVector/MulCoeff.lean | 2 -- Mathlib/Topology/MetricSpace/GromovHausdorff.lean | 2 -- 117 files changed, 243 deletions(-) diff --git a/Archive/Imo/Imo1962Q4.lean b/Archive/Imo/Imo1962Q4.lean index 4789a28129eca..575c66f1a28a7 100644 --- a/Archive/Imo/Imo1962Q4.lean +++ b/Archive/Imo/Imo1962Q4.lean @@ -17,8 +17,6 @@ Since Lean does not have a concept of "simplest form", we just express what is in fact the simplest form of the set of solutions, and then prove it equals the set of solutions. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Real open scoped Real diff --git a/Archive/Imo/Imo2001Q2.lean b/Archive/Imo/Imo2001Q2.lean index 1b8045c2ba72a..3e8528f7ef2ef 100644 --- a/Archive/Imo/Imo2001Q2.lean +++ b/Archive/Imo/Imo2001Q2.lean @@ -32,8 +32,6 @@ open Real variable {a b c : ℝ} -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Imo2001Q2 theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean index 607f73a355f72..32d6e8437a59b 100644 --- a/Archive/Imo/Imo2008Q3.lean +++ b/Archive/Imo/Imo2008Q3.lean @@ -31,8 +31,6 @@ Then `p = 2n + k ≥ 2n + √(p - 4) = 2n + √(2n + k - 4) > √(2n)` and we ar open Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Imo2008Q3 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) : diff --git a/Archive/Imo/Imo2013Q5.lean b/Archive/Imo/Imo2013Q5.lean index 668711c3df3cf..4217b16417651 100644 --- a/Archive/Imo/Imo2013Q5.lean +++ b/Archive/Imo/Imo2013Q5.lean @@ -32,8 +32,6 @@ https://www.imo-official.org/problems/IMO2013SL.pdf open scoped BigOperators -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Imo2013Q5 theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y) diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean index edde9fc8f8d3e..fd3367ae96956 100644 --- a/Archive/Imo/Imo2019Q4.lean +++ b/Archive/Imo/Imo2019Q4.lean @@ -29,8 +29,6 @@ individually. open scoped Nat BigOperators -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Nat hiding zero_le Prime open Finset multiplicity diff --git a/Archive/Wiedijk100Theorems/AbelRuffini.lean b/Archive/Wiedijk100Theorems/AbelRuffini.lean index 33efd6ea814d1..942f926b4464f 100644 --- a/Archive/Wiedijk100Theorems/AbelRuffini.lean +++ b/Archive/Wiedijk100Theorems/AbelRuffini.lean @@ -31,8 +31,6 @@ namespace AbelRuffini set_option linter.uppercaseLean3 false -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Function Polynomial Polynomial.Gal Ideal open scoped Polynomial diff --git a/Archive/Wiedijk100Theorems/AreaOfACircle.lean b/Archive/Wiedijk100Theorems/AreaOfACircle.lean index c98ccfc1e0236..e56ce51c6e24e 100644 --- a/Archive/Wiedijk100Theorems/AreaOfACircle.lean +++ b/Archive/Wiedijk100Theorems/AreaOfACircle.lean @@ -43,9 +43,6 @@ to the n-ball. -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Set Real MeasureTheory intervalIntegral open scoped Real NNReal diff --git a/Archive/Wiedijk100Theorems/HeronsFormula.lean b/Archive/Wiedijk100Theorems/HeronsFormula.lean index 1bf4ced3eb470..81760996b9c26 100644 --- a/Archive/Wiedijk100Theorems/HeronsFormula.lean +++ b/Archive/Wiedijk100Theorems/HeronsFormula.lean @@ -25,8 +25,6 @@ open Real EuclideanGeometry open scoped Real EuclideanGeometry -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Theorems100 local notation "√" => Real.sqrt diff --git a/Mathlib/Analysis/Analytic/RadiusLiminf.lean b/Mathlib/Analysis/Analytic/RadiusLiminf.lean index d93170f504ca4..97fe3033bab65 100644 --- a/Mathlib/Analysis/Analytic/RadiusLiminf.lean +++ b/Mathlib/Analysis/Analytic/RadiusLiminf.lean @@ -27,8 +27,6 @@ open Filter Asymptotics namespace FormalMultilinearSeries -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable (p : FormalMultilinearSeries 𝕜 E F) /-- The radius of a formal multilinear series is equal to diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index 2fc0e3a4a2cbf..f3c8fe8c90b1a 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Basic.lean @@ -712,8 +712,6 @@ theorem integrable_of_continuousOn [CompleteSpace E] {I : Box ι} {f : ℝⁿ variable {l} -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- This is an auxiliary lemma used to prove two statements at once. Use one of the next two lemmas instead. -/ theorem HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann = false) diff --git a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean index 3d452b1cdeacd..839454f631505 100644 --- a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean +++ b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean @@ -139,8 +139,6 @@ theorem norm_volume_sub_integral_face_upper_sub_lower_smul_le {f : (Fin (n + 1) ac_rfl #align box_integral.norm_volume_sub_integral_face_upper_sub_lower_smul_le BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- If `f : ℝⁿ⁺¹ → E` is differentiable on a closed rectangular box `I` with derivative `f'`, then the partial derivative `fun x ↦ f' x (Pi.single i 1)` is Henstock-Kurzweil integrable with integral equal to the difference of integrals of `f` over the faces `x i = I.upper i` and `x i = I.lower i`. diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean b/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean index f10b97172c82f..a16ef72f4bfc0 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean @@ -104,8 +104,6 @@ theorem convolution_tendsto_right_of_continuous {ι} {φ : ι → ContDiffBump ( ((hg.tendsto x₀).comp tendsto_snd) tendsto_const_nhds #align cont_diff_bump.convolution_tendsto_right_of_continuous ContDiffBump.convolution_tendsto_right_of_continuous -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- If a function `g` is locally integrable, then the convolution `φ i * g` converges almost everywhere to `g` if `φ i` is a sequence of bump functions with support tending to `0`, provided that the ratio between the inner and outer radii of `φ i` remains bounded. -/ diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean b/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean index 4554af89c4cdc..e2e42167bd61d 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean @@ -132,8 +132,6 @@ theorem integral_le_measure_closedBall : ∫ x, f x ∂μ ≤ (μ (closedBall c simp [measure_closedBall_lt_top] _ = (μ (closedBall c f.rOut)).toReal := by simp -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - theorem measure_closedBall_div_le_integral [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) : (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ x, f x ∂μ := by have K_pos : 0 < K := by diff --git a/Mathlib/Analysis/Calculus/Monotone.lean b/Mathlib/Analysis/Calculus/Monotone.lean index c9cce07405def..f7db63b63df0d 100644 --- a/Mathlib/Analysis/Calculus/Monotone.lean +++ b/Mathlib/Analysis/Calculus/Monotone.lean @@ -36,8 +36,6 @@ open Set Filter Function Metric MeasureTheory MeasureTheory.Measure IsUnifLocDou open scoped Topology -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- If `(f y - f x) / (y - x)` converges to a limit as `y` tends to `x`, then the same goes if `y` is shifted a little bit, i.e., `f (y + (y-x)^2) - f x) / (y - x)` converges to the same limit. This lemma contains a slightly more general version of this statement (where one considers diff --git a/Mathlib/Analysis/Complex/Liouville.lean b/Mathlib/Analysis/Complex/Liouville.lean index 6138832a29e47..6f1f4a5936224 100644 --- a/Mathlib/Analysis/Complex/Liouville.lean +++ b/Mathlib/Analysis/Complex/Liouville.lean @@ -22,9 +22,6 @@ The proof is based on the Cauchy integral formula for the derivative of an analy `Complex.deriv_eq_smul_circleIntegral`. -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open TopologicalSpace Metric Set Filter Asymptotics Function MeasureTheory Bornology open scoped Topology Filter NNReal Real diff --git a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean index f87fdcfaf2c56..2f23ea2ac1b66 100644 --- a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean +++ b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean @@ -27,8 +27,6 @@ open Set Metric MeasureTheory Filter Complex intervalIntegral open scoped Real Topology -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {E ι : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U K : Set ℂ} {z : ℂ} {M r δ : ℝ} {φ : Filter ι} {F : ι → ℂ → E} {f g : ℂ → E} diff --git a/Mathlib/Analysis/Complex/PhragmenLindelof.lean b/Mathlib/Analysis/Complex/PhragmenLindelof.lean index 529b4f8ddf8ac..339beff93efff 100644 --- a/Mathlib/Analysis/Complex/PhragmenLindelof.lean +++ b/Mathlib/Analysis/Complex/PhragmenLindelof.lean @@ -48,7 +48,6 @@ open Set Function Filter Asymptotics Metric Complex open scoped Topology Filter Real local notation "expR" => Real.exp -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 namespace PhragmenLindelof diff --git a/Mathlib/Analysis/Complex/RemovableSingularity.lean b/Mathlib/Analysis/Complex/RemovableSingularity.lean index 87b921e7ce4b9..d71f6064978d0 100644 --- a/Mathlib/Analysis/Complex/RemovableSingularity.lean +++ b/Mathlib/Analysis/Complex/RemovableSingularity.lean @@ -23,8 +23,6 @@ open TopologicalSpace Metric Set Filter Asymptotics Function open scoped Topology Filter NNReal Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - universe u variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean index 3ca7e9e3e1587..a7f2fd7df0d40 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean @@ -34,9 +34,6 @@ For `p : ℝ`, prove that `fun x ↦ x ^ p` is concave when `0 ≤ p ≤ 1` and `0 < p < 1`. -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Real Set BigOperators NNReal /-- `Real.exp` is strictly convex on the whole real line. diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean index b76484f857883..dddf0f51b9255 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean @@ -34,8 +34,6 @@ open Real Set open scoped BigOperators NNReal -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- `x^n`, `n : ℕ` is strictly convex on `[0, +∞)` for all `n` greater than `2`. -/ theorem strictConvexOn_pow {n : ℕ} (hn : 2 ≤ n) : StrictConvexOn ℝ (Ici 0) fun x : ℝ => x ^ n := by apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _) diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean index 1d79ae3eaeeba..ff3014479bd3a 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean @@ -27,8 +27,6 @@ requires slightly less imports. * Prove convexity for negative powers. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Set namespace NNReal diff --git a/Mathlib/Analysis/Convex/Strong.lean b/Mathlib/Analysis/Convex/Strong.lean index 29196ea1f17b7..19a08901c13cc 100644 --- a/Mathlib/Analysis/Convex/Strong.lean +++ b/Mathlib/Analysis/Convex/Strong.lean @@ -22,8 +22,6 @@ If `E` is an inner product space, this is equivalent to `x ↦ f x - m / 2 * ‖ Prove derivative properties of strongly convex functions. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) - open Real variable {E : Type*} [NormedAddCommGroup E] diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 64e599b97686a..2482dd7af153d 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -58,8 +58,6 @@ The implementation of the seminorms is taken almost literally from `ContinuousLi Schwartz space, tempered distributions -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open scoped BigOperators Nat diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 05f57442e7387..01f27086663af 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -63,8 +63,6 @@ converges to `f` in the uniform-convergence topology of `C(AddCircle T, ℂ)`. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped ENNReal ComplexConjugate Real open TopologicalSpace ContinuousMap MeasureTheory MeasureTheory.Measure Algebra Submodule Set diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index ce581cdfc3f8c..2ac9712a817d8 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -44,8 +44,6 @@ equivalence to an inner-product space. reformulations explicitly using the Fourier integral. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open MeasureTheory Filter Complex Set FiniteDimensional diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 5146670bfd523..30e2a2ccf2ecf 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -40,8 +40,6 @@ adjoint -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open IsROrC diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean index 37023816b8118..d3cb193d705e5 100644 --- a/Mathlib/Analysis/InnerProductSpace/Calculus.lean +++ b/Mathlib/Analysis/InnerProductSpace/Calculus.lean @@ -26,8 +26,6 @@ and from the equivalence of norms in finite dimensions. The last part of the file should be generalized to `PiLp`. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open IsROrC Real Filter diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean index 02265fb1c0be5..4c4566daa77c9 100644 --- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean @@ -53,8 +53,6 @@ For consequences in infinite dimension (Hilbert bases, etc.), see the file -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - set_option linter.uppercaseLean3 false open Real Set Filter IsROrC Submodule Function BigOperators Uniformity Topology NNReal ENNReal diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean index db7b8956d2f7e..b1c5701128299 100644 --- a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean +++ b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean @@ -117,8 +117,6 @@ theorem _root_.LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {T : F variable [CompleteSpace F] {T : F →L[ℝ] F} -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F} (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : F) ‖x₀‖) x₀) : ∃ a b : ℝ, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0 := by diff --git a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean index 2e089c0552cec..107dfd1cb317c 100644 --- a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean +++ b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean @@ -276,8 +276,6 @@ end LinearMap section Nonneg -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - @[simp] theorem inner_product_apply_eigenvector {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : v ∈ Module.End.eigenspace T μ) : ⟪v, T v⟫ = μ * (‖v‖ : 𝕜) ^ 2 := by diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean index c6a4653f6226e..76790944f522a 100644 --- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -74,8 +74,6 @@ open scoped RealInnerProductSpace ComplexConjugate open FiniteDimensional -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - lemma FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (finrank K V = 2)] : FiniteDimensional K V := fact_finiteDimensional_of_finrank_eq_succ 1 diff --git a/Mathlib/Analysis/InnerProductSpace/l2Space.lean b/Mathlib/Analysis/InnerProductSpace/l2Space.lean index 335e886cff793..3f22007c43aea 100644 --- a/Mathlib/Analysis/InnerProductSpace/l2Space.lean +++ b/Mathlib/Analysis/InnerProductSpace/l2Space.lean @@ -88,8 +88,6 @@ open scoped BigOperators NNReal ENNReal Classical ComplexConjugate Topology noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {ι : Type*} variable {𝕜 : Type*} [IsROrC 𝕜] {E : Type*} diff --git a/Mathlib/Analysis/Matrix.lean b/Mathlib/Analysis/Matrix.lean index e027e59356c01..ba4298a004005 100644 --- a/Mathlib/Analysis/Matrix.lean +++ b/Mathlib/Analysis/Matrix.lean @@ -43,9 +43,6 @@ These are not declared as instances because there are several natural choices fo of a matrix. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - - noncomputable section open scoped BigOperators NNReal Matrix diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean index fbb89e827f829..a43245b617b7d 100644 --- a/Mathlib/Analysis/MeanInequalities.lean +++ b/Mathlib/Analysis/MeanInequalities.lean @@ -98,8 +98,6 @@ set_option linter.uppercaseLean3 false noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {ι : Type u} (s : Finset ι) section GeomMeanLEArithMean diff --git a/Mathlib/Analysis/MeanInequalitiesPow.lean b/Mathlib/Analysis/MeanInequalitiesPow.lean index 81e54cc14d9b5..668db2fec9f11 100644 --- a/Mathlib/Analysis/MeanInequalitiesPow.lean +++ b/Mathlib/Analysis/MeanInequalitiesPow.lean @@ -51,8 +51,6 @@ open Classical BigOperators NNReal ENNReal noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {ι : Type u} (s : Finset ι) namespace Real diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean index 53005e65f73d0..879865cb60aca 100644 --- a/Mathlib/Analysis/NormedSpace/PiLp.lean +++ b/Mathlib/Analysis/NormedSpace/PiLp.lean @@ -64,8 +64,6 @@ We also set up the theory for `PseudoEMetricSpace` and `PseudoMetricSpace`. set_option linter.uppercaseLean3 false -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Real Set Filter IsROrC Bornology BigOperators Uniformity Topology NNReal ENNReal noncomputable section diff --git a/Mathlib/Analysis/NormedSpace/ProdLp.lean b/Mathlib/Analysis/NormedSpace/ProdLp.lean index 90329943f5a89..d73bae35d0c9a 100644 --- a/Mathlib/Analysis/NormedSpace/ProdLp.lean +++ b/Mathlib/Analysis/NormedSpace/ProdLp.lean @@ -36,8 +36,6 @@ This files is a straight-forward adaption of `Mathlib.Analysis.NormedSpace.PiLp` -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Real Set Filter IsROrC Bornology BigOperators Uniformity Topology NNReal ENNReal noncomputable section diff --git a/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean b/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean index 3dc379305b4b4..dfbb794b7804e 100644 --- a/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean +++ b/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean @@ -34,8 +34,6 @@ theorem exp_coe (r : ℝ) : exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r) := (map_exp ℝ (algebraMap ℝ ℍ[ℝ]) (continuous_algebraMap _ _) _).symm #align quaternion.exp_coe Quaternion.exp_coe -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- Auxiliary result; if the power series corresponding to `Real.cos` and `Real.sin` evaluated at `‖q‖` tend to `c` and `s`, then the exponential series tends to `c + (s / ‖q‖)`. -/ theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c s : ℝ} diff --git a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean index 46fc975d491c0..cbda220cdd7ec 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean @@ -19,8 +19,6 @@ This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or open scoped BigOperators Matrix -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {𝕜 m n E : Type*} section EntrywiseSupNorm diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean index e2237dccc6878..48f09950910fe 100644 --- a/Mathlib/Analysis/NormedSpace/lpSpace.lean +++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean @@ -57,9 +57,6 @@ say that `‖-f‖ = ‖f‖`, instead of the non-working `f.norm_neg`. set_option autoImplicit true - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open scoped NNReal ENNReal BigOperators Function diff --git a/Mathlib/Analysis/ODE/PicardLindelof.lean b/Mathlib/Analysis/ODE/PicardLindelof.lean index a5b36dfb0cf3f..3916ef0f0ec84 100644 --- a/Mathlib/Analysis/ODE/PicardLindelof.lean +++ b/Mathlib/Analysis/ODE/PicardLindelof.lean @@ -34,8 +34,6 @@ related theorems in `Mathlib/Analysis/ODE/Gronwall.lean`. differential equation -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Filter Function Set Metric TopologicalSpace intervalIntegral MeasureTheory open MeasureTheory.MeasureSpace (volume) open scoped Filter Topology NNReal ENNReal Nat Interval diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean index 2b47876fb71f3..6cd216a11ce1b 100644 --- a/Mathlib/Analysis/PSeries.lean +++ b/Mathlib/Analysis/PSeries.lean @@ -27,9 +27,6 @@ test once we need it. p-series, Cauchy condensation test -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Filter open BigOperators ENNReal NNReal Topology diff --git a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean index bfdf07ab63ca4..c1e33c8b30af2 100644 --- a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean +++ b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean @@ -32,8 +32,6 @@ stronger assumptions (e.g., `im z` is bounded from below and from above) are not open Asymptotics Filter Function open scoped Topology -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Complex /-- We say that `l : Filter ℂ` is an *exponential comparison filter* if the real part tends to diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index ce1ee25526b0e..7076300ca475c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -40,8 +40,6 @@ refined properties of the Gamma function using these relations. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - set_option linter.uppercaseLean3 false open Filter intervalIntegral Set Real MeasureTheory diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean index a3376161986a6..17ddc52cdb969 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean @@ -37,8 +37,6 @@ for positive real `a`, or complex `a` with positive real part. (See also `NumberTheory.ModularForms.JacobiTheta`.) -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open Real Set MeasureTheory Filter Asymptotics diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean index 32799dfd0dbea..2cc20129d5021 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals.lean @@ -37,8 +37,6 @@ open Real Nat Set Finset open scoped Real BigOperators Interval -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {a b : ℝ} (n : ℕ) namespace intervalIntegral diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean index 480202a6c3271..b73d3edc39161 100644 --- a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean +++ b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean @@ -26,7 +26,6 @@ than the dimension. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 open scoped BigOperators NNReal Filter Topology ENNReal open Asymptotics Filter Set Real MeasureTheory FiniteDimensional diff --git a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean index 17d3e4aeed916..b56cae95224bc 100644 --- a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean +++ b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean @@ -22,8 +22,6 @@ It satisfies the following change of variables formula (see `integral_comp_polar noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Real Set MeasureTheory open scoped Real Topology diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean index bac158beefdce..e34623929ee4c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean @@ -13,8 +13,6 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log We construct the power functions `x ^ y`, where `x` and `y` are complex numbers. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220 - open Classical Real Topology Filter ComplexConjugate Finset Set namespace Complex diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean index bdd10ff27c78a..3e679b1e0810f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean @@ -21,8 +21,6 @@ open Classical Real Topology NNReal ENNReal Filter BigOperators ComplexConjugate open Filter Finset Set -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - section CpowLimits /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 7181855ce1ce4..33ac38cdd9b4a 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -18,8 +18,6 @@ We construct the power functions `x ^ y` where We also prove basic properties of these functions. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open Classical Real NNReal ENNReal BigOperators ComplexConjugate diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index 0b5f1c153d95c..373f7578978e4 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -322,8 +322,6 @@ end Complex namespace Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {x y z : ℝ} theorem rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z := by @@ -745,8 +743,6 @@ end Sqrt variable {n : ℕ} -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - theorem exists_rat_pow_btwn_rat_aux (hn : n ≠ 0) (x y : ℝ) (h : x < y) (hy : 0 < y) : ∃ q : ℚ, 0 < q ∧ x < (q : ℝ) ^ n ∧ (q : ℝ) ^ n < y := by have hn' : 0 < (n : ℝ) := by exact_mod_cast hn.bot_lt diff --git a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean index 6799e71dec91e..ac3ec7e95c8cf 100644 --- a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean +++ b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean @@ -27,7 +27,6 @@ cannot have: set_option autoImplicit true -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 noncomputable section open scoped Classical Topology diff --git a/Mathlib/Analysis/SpecialFunctions/Stirling.lean b/Mathlib/Analysis/SpecialFunctions/Stirling.lean index 5ca7c9998f48f..1a94400789a53 100644 --- a/Mathlib/Analysis/SpecialFunctions/Stirling.lean +++ b/Mathlib/Analysis/SpecialFunctions/Stirling.lean @@ -36,8 +36,6 @@ open scoped Topology Real BigOperators Nat open Finset Filter Nat Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Stirling /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean index 34233bc6a0c1f..14ef64ab59143 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean @@ -17,8 +17,6 @@ and `Real.tan` as a `LocalHomeomorph` between `(-(π / 2), π / 2)` and the whol noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Real open Set Filter diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean index 3fe76c99a7630..d396d8eef2484 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean @@ -17,8 +17,6 @@ Continuity and derivatives of the tangent and arctangent functions. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Real open Set Filter diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean index 3b09875f83f53..a48ff98741474 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean @@ -33,8 +33,6 @@ sin, cos, tan, angle noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Set namespace Real diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean index e776100272383..5329e884426ca 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean @@ -121,8 +121,6 @@ theorem tan_add' {x y : ℂ} tan_add (Or.inl h) #align complex.tan_add' Complex.tan_add' -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - theorem tan_two_mul {z : ℂ} : tan (2 * z) = (2 : ℂ) * tan z / ((1 : ℂ) - tan z ^ 2) := by by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2 · rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)] diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean index 2678cb0e3bcd9..1af7485b9511d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean @@ -16,8 +16,6 @@ Basic facts and derivatives for the complex trigonometric functions. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Complex open Set Filter diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean index 743f6583cf95a..751fcf1076166 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean @@ -20,9 +20,6 @@ is to prove a recurrence relation for the integrals `∫ x in 0..π/2, cos 2 z x generalising the arguments used to prove Wallis' limit formula for `π`. -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped Real Topology BigOperators open Real Set Filter intervalIntegral MeasureTheory.MeasureSpace diff --git a/Mathlib/Analysis/SpecificLimits/FloorPow.lean b/Mathlib/Analysis/SpecificLimits/FloorPow.lean index 5473de4519869..82ea4049d0a68 100644 --- a/Mathlib/Analysis/SpecificLimits/FloorPow.lean +++ b/Mathlib/Analysis/SpecificLimits/FloorPow.lean @@ -19,8 +19,6 @@ We state several auxiliary results pertaining to sequences of the form `⌊c^n to `1/j^2`, up to a multiplicative constant. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Filter Finset open Topology BigOperators diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean index 29b165534b363..0725f50222aac 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean @@ -32,8 +32,6 @@ This entire file is internal to the proof of Szemerédi Regularity Lemma. open Finset Fintype Function Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open BigOperators namespace SzemerediRegularity diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean index 0ec26e2331238..3cf2eb73c6258 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean @@ -39,8 +39,6 @@ Once ported to mathlib4, this file will be a great golfing ground for Heather's open Finpartition Finset Fintype Rel Nat -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped BigOperators Classical SzemerediRegularity.Positivity namespace SzemerediRegularity diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean index d43461750de92..bb0328a90275a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean @@ -32,8 +32,6 @@ open BigOperators variable {α : Type*} [DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α) [DecidableRel G.Adj] -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace Finpartition /-- The energy of a partition, also known as index. Auxiliary quantity for Szemerédi's regularity diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean index d16579fa938ef..52bdbf2c8f142 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean @@ -38,8 +38,6 @@ Once ported to mathlib4, this file will be a great golfing ground for Heather's open Finset Fintype SimpleGraph SzemerediRegularity -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped BigOperators Classical SzemerediRegularity.Positivity variable {α : Type*} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition) diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean index 8a4ccf0de75c3..abceb6ec375e3 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean @@ -68,8 +68,6 @@ open Finpartition Finset Fintype Function SzemerediRegularity open scoped Classical -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {α : Type*} [Fintype α] (G : SimpleGraph α) {ε : ℝ} {l : ℕ} /-- Effective **Szemerédi Regularity Lemma**: For any sufficiently large graph, there is an diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean index 974adb6df890b..f068e176455cb 100644 --- a/Mathlib/Data/PNat/Basic.lean +++ b/Mathlib/Data/PNat/Basic.lean @@ -20,8 +20,6 @@ It is defined in `Data.PNat.Defs`, but most of the development is deferred to he that `Data.PNat.Defs` can have very few imports. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - deriving instance AddLeftCancelSemigroup, AddRightCancelSemigroup, AddCommSemigroup, LinearOrderedCancelCommMonoid, Add, Mul, Distrib for PNat diff --git a/Mathlib/Data/Real/Pi/Bounds.lean b/Mathlib/Data/Real/Pi/Bounds.lean index 34d0be3eeddae..11e758316ab7a 100644 --- a/Mathlib/Data/Real/Pi/Bounds.lean +++ b/Mathlib/Data/Real/Pi/Bounds.lean @@ -19,8 +19,6 @@ See also `Mathlib/Data/Real/Pi/Leibniz.lean` and `Mathlib/Data/Real/Pi/Wallis.le formulas for `π`. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - -- Porting note: needed to add a lot of type ascriptions for lean to interpret numbers as reals. open scoped Real diff --git a/Mathlib/Data/Real/Pi/Leibniz.lean b/Mathlib/Data/Real/Pi/Leibniz.lean index b2119ea2a569c..644b510307692 100644 --- a/Mathlib/Data/Real/Pi/Leibniz.lean +++ b/Mathlib/Data/Real/Pi/Leibniz.lean @@ -12,8 +12,6 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv namespace Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Filter Set open scoped Classical BigOperators Topology Real diff --git a/Mathlib/Data/Real/Pi/Wallis.lean b/Mathlib/Data/Real/Pi/Wallis.lean index 89b3317cb4aa1..0fd4d8a5e2324 100644 --- a/Mathlib/Data/Real/Pi/Wallis.lean +++ b/Mathlib/Data/Real/Pi/Wallis.lean @@ -40,8 +40,6 @@ namespace Real namespace Wallis -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - set_option linter.uppercaseLean3 false /-- The product of the first `k` terms in Wallis' formula for `π`. -/ diff --git a/Mathlib/Data/ZMod/IntUnitsPower.lean b/Mathlib/Data/ZMod/IntUnitsPower.lean index 79ff46b5386a0..b32f06053f921 100644 --- a/Mathlib/Data/ZMod/IntUnitsPower.lean +++ b/Mathlib/Data/ZMod/IntUnitsPower.lean @@ -24,8 +24,6 @@ by using `Module R (Additive M)` in its place, especially since this already has `R = ℕ` and `R = ℤ`. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - instance : SMul (ZMod 2) (Additive ℤˣ) where smul z au := .ofMul <| Additive.toMul au ^ z.val diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index 72aa3447d9a58..b2b4f917664b1 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/Mathlib/FieldTheory/AbelRuffini.lean @@ -28,8 +28,6 @@ that is solvable by radicals has a solvable Galois group. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped Classical Polynomial IntermediateField open Polynomial IntermediateField diff --git a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean index 923e92883b264..be981014ed60d 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean @@ -35,8 +35,6 @@ eigenvalue. * `σ a` : `spectrum R a` of `a : A` -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace spectrum open Set Polynomial diff --git a/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean b/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean index 2f81705007ce4..a27f45ae1fad7 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean @@ -29,8 +29,6 @@ triangle unnecessarily. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped BigOperators open scoped EuclideanGeometry diff --git a/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean b/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean index 6520cf3a25b19..1ed3db1cb6c30 100644 --- a/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean +++ b/Mathlib/Geometry/Euclidean/Inversion/Calculus.lean @@ -22,8 +22,6 @@ space in this file. inversion, derivative -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Metric Function AffineMap Set AffineSubspace open scoped Topology RealInnerProductSpace diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index afe5d98760c97..940d0fe174958 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/Mathlib/Geometry/Euclidean/Triangle.lean @@ -38,8 +38,6 @@ unnecessarily. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped BigOperators open scoped Classical diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index 9f029a7275572..c45388ea58b2b 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -72,8 +72,6 @@ open Metric FiniteDimensional Function open scoped Manifold -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - section StereographicProjection variable (v : E) diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index 6896c11de78b5..07f6e3bcf347f 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -56,8 +56,6 @@ linear algebra, vector space, module -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Function open BigOperators Pointwise diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean index e6498ba76c448..d9a02f2a4eeee 100644 --- a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean +++ b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean @@ -44,8 +44,6 @@ In particular, this number is bounded by `5 ^ dim` by a straightforward measure universe u -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Metric Set FiniteDimensional MeasureTheory Filter Fin open scoped ENNReal Topology diff --git a/Mathlib/MeasureTheory/Covering/Differentiation.lean b/Mathlib/MeasureTheory/Covering/Differentiation.lean index fb8216b9e25c0..69ad5fc5071f5 100644 --- a/Mathlib/MeasureTheory/Covering/Differentiation.lean +++ b/Mathlib/MeasureTheory/Covering/Differentiation.lean @@ -76,9 +76,6 @@ make no sense. However, the measure is not globally zero if the space is big eno * [Herbert Federer, Geometric Measure Theory, Chapter 2.9][Federer1996] -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open MeasureTheory Metric Set Filter TopologicalSpace MeasureTheory.Measure open scoped Filter ENNReal MeasureTheory NNReal Topology diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean index fe2e0cf08bec2..03eb8fbdac493 100644 --- a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean +++ b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean @@ -139,8 +139,6 @@ theorem tendstoInMeasure_of_tendsto_ae [IsFiniteMeasure μ] (hf : ∀ n, AEStron exact hxfg #align measure_theory.tendsto_in_measure_of_tendsto_ae MeasureTheory.tendstoInMeasure_of_tendsto_ae -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace ExistsSeqTendstoAe theorem exists_nat_measure_lt_two_inv (hfg : TendstoInMeasure μ f atTop g) (n : ℕ) : diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index d2f3721665fee..0d15e8586c59c 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -88,9 +88,6 @@ Change of variables in integrals [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2] -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open MeasureTheory MeasureTheory.Measure Metric Filter Set FiniteDimensional Asymptotics TopologicalSpace diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean index 0e82a13ad9748..2b4e7062e3bed 100644 --- a/Mathlib/MeasureTheory/Function/L2Space.lean +++ b/Mathlib/MeasureTheory/Function/L2Space.lean @@ -24,9 +24,6 @@ is also an inner product space, with inner product defined as `inner f g = ∫ a -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - set_option linter.uppercaseLean3 false noncomputable section diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 638e7afef7b0b..406af852e0d74 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -68,8 +68,6 @@ open TopologicalSpace MeasureTheory Filter open scoped NNReal ENNReal BigOperators Topology MeasureTheory Uniformity -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {α E F G : Type*} {m m0 : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] diff --git a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean index 1b3204cd2edb2..41d3cea0a3c24 100644 --- a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean @@ -71,8 +71,6 @@ integral, circle, Cauchy integral variable {E : Type*} [NormedAddCommGroup E] -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open scoped Real NNReal Interval Pointwise Topology diff --git a/Mathlib/MeasureTheory/Integral/CircleTransform.lean b/Mathlib/MeasureTheory/Integral/CircleTransform.lean index 4996f048a5c32..ce63978006ba4 100644 --- a/Mathlib/MeasureTheory/Integral/CircleTransform.lean +++ b/Mathlib/MeasureTheory/Integral/CircleTransform.lean @@ -25,8 +25,6 @@ open Set MeasureTheory Metric Filter Function open scoped Interval Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] (R : ℝ) (z w : ℂ) diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean index b5a9582183f7b..3fd8394c65129 100644 --- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean +++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean @@ -58,8 +58,6 @@ open Classical BigOperators NNReal ENNReal MeasureTheory Finset set_option linter.uppercaseLean3 false -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {α : Type*} [MeasurableSpace α] {μ : Measure α} namespace ENNReal diff --git a/Mathlib/MeasureTheory/Integral/PeakFunction.lean b/Mathlib/MeasureTheory/Integral/PeakFunction.lean index 8f268aa102add..864de31622f76 100644 --- a/Mathlib/MeasureTheory/Integral/PeakFunction.lean +++ b/Mathlib/MeasureTheory/Integral/PeakFunction.lean @@ -30,9 +30,6 @@ Note that there are related results about convolution with respect to peak funct `Analysis.Convolution`, such as `convolution_tendsto_right` there. -/ - -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Set Filter MeasureTheory MeasureTheory.Measure TopologicalSpace Metric open scoped Topology ENNReal diff --git a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean index 5e51e0229c33e..3c30e440df088 100644 --- a/Mathlib/MeasureTheory/Integral/TorusIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/TorusIntegral.lean @@ -71,7 +71,6 @@ local macro:arg t:term:max noWs "ⁿ⁺¹" : term => `(Fin (n + 1) → $t) local macro:arg t:term:max noWs "ⁿ" : term => `(Fin n → $t) local macro:arg t:term:max noWs "⁰" : term => `(Fin 0 → $t) local macro:arg t:term:max noWs "¹" : term => `(Fin 1 → $t) -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 /-! ### `torusMap`, a parametrization of a torus diff --git a/Mathlib/MeasureTheory/Measure/Doubling.lean b/Mathlib/MeasureTheory/Measure/Doubling.lean index 0318c1fadd650..8e059bccb4200 100644 --- a/Mathlib/MeasureTheory/Measure/Doubling.lean +++ b/Mathlib/MeasureTheory/Measure/Doubling.lean @@ -25,9 +25,6 @@ This file records basic facts about uniformly locally doubling measures. appearing in the definition of a uniformly locally doubling measure. -/ --- Porting note: for 2 ^ n in exists_eventually_forall_measure_closedBall_le_mul -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open Set Filter Metric MeasureTheory TopologicalSpace ENNReal NNReal Topology diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index a4f75ce89df44..84c4d839314a1 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean @@ -20,8 +20,6 @@ measure `1` to the parallelepiped spanned by any orthonormal basis, and that it the canonical `volume` from the `MeasureSpace` instance. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open FiniteDimensional MeasureTheory MeasureTheory.Measure Set variable {ι F : Type*} diff --git a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean index f4f059be045a2..2e82754471020 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean @@ -13,8 +13,6 @@ import Mathlib.MeasureTheory.Integral.Bochner -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open scoped NNReal ENNReal Pointwise BigOperators Topology diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean index a4dc0e5d2c72d..87bf58908cee9 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean @@ -34,8 +34,6 @@ assert_not_exists MeasureTheory.integral noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Classical Set Filter MeasureTheory MeasureTheory.Measure TopologicalSpace open ENNReal (ofReal) diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean index 651fdd187fec4..a0188da934236 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean @@ -20,8 +20,6 @@ used ways to represent `ℝ²` in `mathlib`: `ℝ × ℝ` and `Fin 2 → ℝ`, d of `MeasureTheory.measurePreserving`). -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open MeasureTheory noncomputable section diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index a13b76264fdf4..70d9b5a7e7066 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -43,8 +43,6 @@ density one for the rescaled copies `{x} + r • t` of a given set `t` with posi small `r`, see `eventually_nonempty_inter_smul_of_density_one`. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - assert_not_exists MeasureTheory.integral open TopologicalSpace Set Filter Metric Bornology diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index 17d08ac9eb5f7..4b2a572e75008 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -23,8 +23,6 @@ We compute the discriminant of a `p ^ n`-th cyclotomic extension. universe u v -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open Algebra Polynomial Nat IsPrimitiveRoot PowerBasis open scoped Polynomial Cyclotomic diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 5b2b78cc50727..b0fd00ba38d07 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -72,7 +72,6 @@ variable {p n : ℕ+} (A : Type w) (B : Type z) (K : Type u) {L : Type v} (C : T variable [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 section Zeta namespace IsCyclotomicExtension diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index 8819be702853b..ec0cadec1d3cf 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -30,8 +30,6 @@ open scoped Cyclotomic NumberField Nat variable {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (p : ℕ).Prime] -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace IsCyclotomicExtension.Rat /-- The discriminant of the power basis given by `ζ - 1`. -/ diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index ffd1d3f8e681d..ffc5aa0a931b5 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -19,8 +19,6 @@ open Finset Nat open scoped BigOperators Nat -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - section GaussEisenstein namespace ZMod diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean index dabb8385867ce..005ffa818ccd2 100644 --- a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean +++ b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean @@ -337,8 +337,6 @@ namespace Liouville variable {x : ℝ} -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- If `x` is a Liouville number, then for any `n`, for infinitely many denominators `b` there exists a numerator `a` such that `x ≠ a / b` and `|x - a / b| < 1 / b ^ n`. -/ theorem frequently_exists_num (hx : Liouville x) (n : ℕ) : diff --git a/Mathlib/NumberTheory/Liouville/Measure.lean b/Mathlib/NumberTheory/Liouville/Measure.lean index fbfb674f40a19..70318cdd9405d 100644 --- a/Mathlib/NumberTheory/Liouville/Measure.lean +++ b/Mathlib/NumberTheory/Liouville/Measure.lean @@ -31,8 +31,6 @@ open scoped Filter BigOperators ENNReal Topology NNReal open Filter Set Metric MeasureTheory Real -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - theorem setOf_liouvilleWith_subset_aux : { x : ℝ | ∃ p > 2, LiouvilleWith p x } ⊆ ⋃ m : ℤ, (· + (m : ℝ)) ⁻¹' ⋃ n > (0 : ℕ), diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean index d41d40b3f977f..f01c50e9f5070 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean @@ -26,8 +26,6 @@ open Complex Real Asymptotics Filter open scoped Real BigOperators UpperHalfPlane -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- Jacobi's theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/ noncomputable def jacobiTheta (z : ℂ) : ℂ := ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * z) diff --git a/Mathlib/NumberTheory/ModularForms/SlashActions.lean b/Mathlib/NumberTheory/ModularForms/SlashActions.lean index 2a417e3e8ab96..50c6c2484f6da 100644 --- a/Mathlib/NumberTheory/ModularForms/SlashActions.lean +++ b/Mathlib/NumberTheory/ModularForms/SlashActions.lean @@ -29,8 +29,6 @@ open Complex UpperHalfPlane open scoped UpperHalfPlane -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - local notation "GL(" n ", " R ")" "⁺" => Matrix.GLPos (Fin n) R local notation "SL(" n ", " R ")" => Matrix.SpecialLinearGroup (Fin n) R diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 7c1fad2fe1be1..722fb0b0fe4ea 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -32,8 +32,6 @@ for `x ∈ K`, we have `Π_w ‖x‖_w = |norm(x)|` where the product is over th number field, embeddings, places, infinite places -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped Classical namespace NumberField.Embeddings diff --git a/Mathlib/NumberTheory/SumFourSquares.lean b/Mathlib/NumberTheory/SumFourSquares.lean index dae91282da785..f03d351084a61 100644 --- a/Mathlib/NumberTheory/SumFourSquares.lean +++ b/Mathlib/NumberTheory/SumFourSquares.lean @@ -27,8 +27,6 @@ open Finset Polynomial FiniteField Equiv open scoped BigOperators -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- **Euler's four-square identity**. -/ theorem euler_four_squares {R : Type*} [CommRing R] (a b c d x y z w : R) : (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + diff --git a/Mathlib/NumberTheory/ZetaFunction.lean b/Mathlib/NumberTheory/ZetaFunction.lean index 18a650a539655..c4a8e637a4079 100644 --- a/Mathlib/NumberTheory/ZetaFunction.lean +++ b/Mathlib/NumberTheory/ZetaFunction.lean @@ -68,8 +68,6 @@ noncomputable section ## Definition of the Riemann zeta function and related functions -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- Function whose Mellin transform is `π ^ (-s) * Γ(s) * zeta (2 * s)`, for `1 / 2 < Re s`. -/ def zetaKernel₁ (t : ℝ) : ℂ := ∑' n : ℕ, rexp (-π * t * ((n : ℝ) + 1) ^ 2) diff --git a/Mathlib/NumberTheory/ZetaValues.lean b/Mathlib/NumberTheory/ZetaValues.lean index 0bb51cb562bc0..d7a3a24358cf0 100644 --- a/Mathlib/NumberTheory/ZetaValues.lean +++ b/Mathlib/NumberTheory/ZetaValues.lean @@ -28,8 +28,6 @@ zeta functions, in terms of Bernoulli polynomials. an explicit multiple of `Bₖ(x)`, for any `x ∈ [0, 1]` and `k ≥ 3` odd. -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - noncomputable section open scoped Nat Real Interval diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean index 93e1830904d1b..25e3a6ae228d8 100644 --- a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean +++ b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean @@ -23,8 +23,6 @@ open Zsqrtd Complex open scoped ComplexConjugate -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - local notation "ℤ[i]" => GaussianInt namespace GaussianInt diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean index ff463656637fe..47dab0e747bf9 100644 --- a/Mathlib/Probability/Distributions/Gaussian.lean +++ b/Mathlib/Probability/Distributions/Gaussian.lean @@ -34,8 +34,6 @@ open scoped ENNReal NNReal Real open MeasureTheory -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace ProbabilityTheory section GaussianPdf diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean index 57580ccf3cf08..5c375c2d228f9 100644 --- a/Mathlib/Probability/StrongLaw.lean +++ b/Mathlib/Probability/StrongLaw.lean @@ -57,8 +57,6 @@ random variables. Let `Yₙ` be the truncation of `Xₙ` up to `n`. We claim tha noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open MeasureTheory Filter Finset Asymptotics open Set (indicator) diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean index 9b7c1ca11b368..64c0ec5432091 100644 --- a/Mathlib/Probability/Variance.lean +++ b/Mathlib/Probability/Variance.lean @@ -43,8 +43,6 @@ open scoped BigOperators MeasureTheory ProbabilityTheory ENNReal NNReal namespace ProbabilityTheory -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - -- Porting note: this lemma replaces `ENNReal.toReal_bit0`, which does not exist in Lean 4 private lemma coe_two : ENNReal.toReal 2 = (2 : ℝ) := rfl diff --git a/Mathlib/RingTheory/LocalProperties.lean b/Mathlib/RingTheory/LocalProperties.lean index 35b8347cfffef..35d60ea2461a3 100644 --- a/Mathlib/RingTheory/LocalProperties.lean +++ b/Mathlib/RingTheory/LocalProperties.lean @@ -38,8 +38,6 @@ The following properties are covered: -/ -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - open scoped Pointwise Classical BigOperators universe u diff --git a/Mathlib/RingTheory/Polynomial/Selmer.lean b/Mathlib/RingTheory/Polynomial/Selmer.lean index 7d54d57060f47..7a6453a002f82 100644 --- a/Mathlib/RingTheory/Polynomial/Selmer.lean +++ b/Mathlib/RingTheory/Polynomial/Selmer.lean @@ -26,8 +26,6 @@ namespace Polynomial open scoped Polynomial -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - variable {n : ℕ} theorem X_pow_sub_X_sub_one_irreducible_aux (z : ℂ) : ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0) := by diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index 437e9f93e2342..de71cc5cfb363 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -265,8 +265,6 @@ section Reduced variable (R) [CommRing R] [IsReduced R] -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - -- @[simp] -- Porting note: simp normal form is `mem_rootsOfUnity_prime_pow_mul_iff'` theorem mem_rootsOfUnity_prime_pow_mul_iff (p k : ℕ) (m : ℕ+) [hp : Fact p.Prime] [CharP R p] {ζ : Rˣ} : ζ ∈ rootsOfUnity (⟨p, hp.1.pos⟩ ^ k * m) R ↔ ζ ∈ rootsOfUnity m R := by diff --git a/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean b/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean index 511e717d8c5ac..554e2051aead4 100644 --- a/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean +++ b/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean @@ -30,8 +30,6 @@ When `k` is also a field, this `b` can be chosen to be a unit of `𝕎 k`. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace WittVector variable {p : ℕ} [hp : Fact p.Prime] diff --git a/Mathlib/RingTheory/WittVector/MulCoeff.lean b/Mathlib/RingTheory/WittVector/MulCoeff.lean index 48f1d191b3a68..3a4d3d8c08159 100644 --- a/Mathlib/RingTheory/WittVector/MulCoeff.lean +++ b/Mathlib/RingTheory/WittVector/MulCoeff.lean @@ -30,8 +30,6 @@ that needs to happen in characteristic 0. noncomputable section -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - namespace WittVector variable (p : ℕ) [hp : Fact p.Prime] diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorff.lean b/Mathlib/Topology/MetricSpace/GromovHausdorff.lean index 5892b5fd90c3a..0d264332d7b9a 100644 --- a/Mathlib/Topology/MetricSpace/GromovHausdorff.lean +++ b/Mathlib/Topology/MetricSpace/GromovHausdorff.lean @@ -1002,8 +1002,6 @@ def auxGluing (n : ℕ) : AuxGluingStruct (X n) := isom := (toGlueR_isometry _ _).comp (isometry_optimalGHInjr (X n) (X (n + 1))) } #align Gromov_Hausdorff.aux_gluing GromovHausdorff.auxGluing -local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 - /-- The Gromov-Hausdorff space is complete. -/ instance : CompleteSpace GHSpace := by set d := fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n From a55f2067d6703efab7c72c6dcd797d6c6b04057d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 27 Oct 2023 19:04:06 -0700 Subject: [PATCH 03/10] copy some fixes from #6852 --- Archive/Sensitivity.lean | 2 +- .../Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean | 2 +- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean | 2 +- Mathlib/Algebra/CharP/LocalRing.lean | 2 +- Mathlib/Algebra/CharZero/Quotient.lean | 2 +- Mathlib/Algebra/Group/Defs.lean | 5 +++++ Mathlib/Algebra/Module/DedekindDomain.lean | 6 +++--- Mathlib/Algebra/Module/Injective.lean | 2 +- Mathlib/Algebra/Order/Interval.lean | 2 +- Mathlib/Algebra/Order/Positive/Ring.lean | 2 +- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean | 2 +- Mathlib/CategoryTheory/Action.lean | 2 +- Mathlib/Data/Int/Bitwise.lean | 4 ++-- Mathlib/Data/PNat/Prime.lean | 2 +- Mathlib/Data/Rat/Cast/CharZero.lean | 2 +- Mathlib/GroupTheory/GroupAction/Quotient.lean | 2 +- Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean | 4 ++-- Mathlib/GroupTheory/Submonoid/Operations.lean | 2 +- Mathlib/LinearAlgebra/Alternating/Basic.lean | 3 +-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean | 2 +- Mathlib/Topology/Algebra/Module/Basic.lean | 4 ++-- 21 files changed, 30 insertions(+), 26 deletions(-) diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index 930668edaeaec..2a287f60c17a5 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -401,7 +401,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) : let img := range (g m) suffices 0 < dim (W ⊓ img) by exact_mod_cast exists_mem_ne_zero_of_rank_pos this - have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1) := by + have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1 : Cardinal) := by convert ← rank_submodule_le (W ⊔ img) rw [← Nat.cast_succ] apply dim_V diff --git a/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean b/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean index 05b6a23992908..e91db756e5796 100644 --- a/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean +++ b/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean @@ -240,7 +240,7 @@ theorem Real.tendsto_sum_one_div_prime_atTop : have h4 := calc (card M' : ℝ) ≤ 2 ^ k * x.sqrt := by exact_mod_cast card_le_two_pow_mul_sqrt - _ = 2 ^ k * ↑(2 ^ (k + 1)) := by rw [Nat.sqrt_eq] + _ = 2 ^ k * (2 ^ (k + 1) : ℕ) := by rw [Nat.sqrt_eq] _ = x / 2 := by field_simp [mul_right_comm, ← pow_succ'] refine' lt_irrefl (x : ℝ) _ calc diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean index 01c59b6fc2708..1a45c9f556f84 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean @@ -287,7 +287,7 @@ protected theorem coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algeb @[simp, norm_cast] theorem coe_smul [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : S) : - (r • x : A) = r • (x : A) := + ↑(r • x) = r • (x : A) := rfl protected theorem coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 := diff --git a/Mathlib/Algebra/CharP/LocalRing.lean b/Mathlib/Algebra/CharP/LocalRing.lean index 2b4137755a246..a932451a0ca01 100644 --- a/Mathlib/Algebra/CharP/LocalRing.lean +++ b/Mathlib/Algebra/CharP/LocalRing.lean @@ -51,7 +51,7 @@ theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [LocalRing R] (q : -- Let `b` be the inverse of `a`. cases' a_unit.exists_left_inv with a_inv h_inv_mul_a have rn_cast_zero : ↑(r ^ n) = (0 : R) := by - rw [← @mul_one R _ (r ^ n), mul_comm, ←Classical.choose_spec a_unit.exists_left_inv, + rw [← @mul_one R _ ↑(r ^ n), mul_comm, ←Classical.choose_spec a_unit.exists_left_inv, mul_assoc, ← Nat.cast_mul, ←q_eq_a_mul_rn, CharP.cast_eq_zero R q] simp have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean index d46c5853c577f..8bcfbf76d972c 100644 --- a/Mathlib/Algebra/CharZero/Quotient.lean +++ b/Mathlib/Algebra/CharZero/Quotient.lean @@ -53,7 +53,7 @@ end AddSubgroup namespace QuotientAddGroup theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) : - z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + (k : ℕ) • (p / z : R) := by + z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z : R) :) := by induction ψ using Quotient.inductionOn' induction θ using Quotient.inductionOn' -- Porting note: Introduced Zp notation to shorten lines diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index d172e8d355f9d..1be3f043a74b4 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -56,6 +56,9 @@ class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where /-- The notation typeclass for heterogeneous scalar multiplication. This enables the notation `a • b : γ` where `a : α`, `b : β`. + +It is assumed to represent an action on the left in some sense. +When elaborating `a • b`, coercions get propagated to `b` and not to `a`. -/ class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where /-- `a • b` computes the product of `a` and `b`. @@ -86,6 +89,8 @@ infixl:65 " +ᵥ " => HVAdd.hVAdd infixl:65 " -ᵥ " => VSub.vsub infixr:73 " • " => HSMul.hSMul +macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y) + attribute [to_additive existing] Mul Div HMul instHMul HDiv instHDiv HSMul attribute [to_additive (reorder := 1 2) SMul] Pow attribute [to_additive (reorder := 1 2)] HPow diff --git a/Mathlib/Algebra/Module/DedekindDomain.lean b/Mathlib/Algebra/Module/DedekindDomain.lean index 9fc146976d910..999d73a16f4f2 100644 --- a/Mathlib/Algebra/Module/DedekindDomain.lean +++ b/Mathlib/Algebra/Module/DedekindDomain.lean @@ -39,7 +39,7 @@ torsion submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M I) : DirectSum.IsInternal fun p : (factors I).toFinset => - torsionBySet R M ((p : Ideal R) ^ (factors I).count ↑p) := by + torsionBySet R M (p ^ (factors I).count ↑p : Ideal R) := by let P := factors I have prime_of_mem := fun p (hp : p ∈ P.toFinset) => prime_of_factor p (Multiset.mem_toFinset.mp hp) @@ -66,7 +66,7 @@ theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI `e i` are their multiplicities. -/ theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset => - torsionBySet R M ((p : Ideal R) ^ (factors (⊤ : Submodule R M).annihilator).count ↑p) := by + torsionBySet R M (p ^ (factors (⊤ : Submodule R M).annihilator).count ↑p : Ideal R) := by have hM' := Module.isTorsionBySet_annihilator_top R M have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM refine' isInternal_prime_power_torsion_of_is_torsion_by_ideal _ hM' @@ -78,7 +78,7 @@ theorem isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsio `p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`.-/ theorem exists_isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) : ∃ (P : Finset <| Ideal R) (_ : DecidableEq P) (_ : ∀ p ∈ P, Prime p) (e : P → ℕ), - DirectSum.IsInternal fun p : P => torsionBySet R M ((p : Ideal R) ^ e p) := + DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) := ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _, isInternal_prime_power_torsion hM⟩ #align submodule.exists_is_internal_prime_power_torsion Submodule.exists_isInternal_prime_power_torsion diff --git a/Mathlib/Algebra/Module/Injective.lean b/Mathlib/Algebra/Module/Injective.lean index 1682aa34aca48..f9ea188004147 100644 --- a/Mathlib/Algebra/Module/Injective.lean +++ b/Mathlib/Algebra/Module/Injective.lean @@ -415,7 +415,7 @@ def extensionOfMaxAdjoin (h : Module.Baer R Q) (y : N) : ExtensionOf i f where ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y := by rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul] rfl - rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a) _ _ eq1, LinearMap.map_smul, + rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, LinearMap.map_smul, LinearPMap.map_smul, ← smul_add] congr } is_extension m := by diff --git a/Mathlib/Algebra/Order/Interval.lean b/Mathlib/Algebra/Order/Interval.lean index 2d26ed32e73b9..207ef40c4cd73 100644 --- a/Mathlib/Algebra/Order/Interval.lean +++ b/Mathlib/Algebra/Order/Interval.lean @@ -304,7 +304,7 @@ namespace NonemptyInterval @[to_additive] theorem coe_pow_interval [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ℕ) : - (s ^ n : Interval α) = (s : Interval α) ^ n := + ↑(s ^ n) = (s : Interval α) ^ n := map_pow (⟨⟨(↑), coe_one_interval⟩, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _ _ #align nonempty_interval.coe_pow_interval NonemptyInterval.coe_pow_interval #align nonempty_interval.coe_nsmul_interval NonemptyInterval.coe_nsmul_interval diff --git a/Mathlib/Algebra/Order/Positive/Ring.lean b/Mathlib/Algebra/Order/Positive/Ring.lean index a9f802372208f..8d32a13e2effa 100644 --- a/Mathlib/Algebra/Order/Positive/Ring.lean +++ b/Mathlib/Algebra/Order/Positive/Ring.lean @@ -109,7 +109,7 @@ instance : Pow { x : R // 0 < x } ℕ := @[simp] theorem val_pow (x : { x : R // 0 < x }) (n : ℕ) : - (x ^ n : R) = (x : R) ^ n := + ↑(x ^ n) = (x : R) ^ n := rfl #align positive.coe_pow Positive.val_pow diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean index 8d9593f34a29a..d1007945a9f41 100644 --- a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean +++ b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean @@ -282,7 +282,7 @@ protected theorem coe_sub {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing @[simp, norm_cast] theorem coe_smul [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : S) : - (r • x : A) = r • (x : A) := + ↑(r • x) = r • (x : A) := rfl protected theorem coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 := diff --git a/Mathlib/CategoryTheory/Action.lean b/Mathlib/CategoryTheory/Action.lean index 99cccd566b98e..80c5b00afa6c0 100644 --- a/Mathlib/CategoryTheory/Action.lean +++ b/Mathlib/CategoryTheory/Action.lean @@ -160,7 +160,7 @@ def endMulEquivSubgroup (H : Subgroup G) : End (objEquiv G (G ⧸ H) ↑(1 : G)) #align category_theory.action_category.End_mul_equiv_subgroup CategoryTheory.ActionCategory.endMulEquivSubgroup /-- A target vertex `t` and a scalar `g` determine a morphism in the action groupoid. -/ -def homOfPair (t : X) (g : G) : @Quiver.Hom (ActionCategory G X) _ (g⁻¹ • t) t := +def homOfPair (t : X) (g : G) : @Quiver.Hom (ActionCategory G X) _ (g⁻¹ • t :) t := Subtype.mk g (smul_inv_smul g t) #align category_theory.action_category.hom_of_pair CategoryTheory.ActionCategory.homOfPair diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index b39481fe6a610..f776c5598e108 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -432,12 +432,12 @@ theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (n - k) = (m <<< (n shiftLeft_add _ _ _ #align int.shiftl_sub Int.shiftLeft_sub -theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * ↑(2 ^ n) +theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ) | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp) | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _) #align int.shiftl_eq_mul_pow Int.shiftLeft_eq_mul_pow -theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / ↑(2 ^ n) +theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / (2 ^ n : ℕ) | (m : ℕ), n => by rw [shiftRight_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp | -[m+1], n => by rw [shiftRight_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl diff --git a/Mathlib/Data/PNat/Prime.lean b/Mathlib/Data/PNat/Prime.lean index 17ef5e3afe5dd..ed2740dd7d6c8 100644 --- a/Mathlib/Data/PNat/Prime.lean +++ b/Mathlib/Data/PNat/Prime.lean @@ -295,7 +295,7 @@ theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m := by apply Nat.gcd_eq_left h #align pnat.gcd_eq_left PNat.gcd_eq_left -theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k).Coprime (n ^ l) := by +theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k : ℕ).Coprime (n ^ l) := by rw [← coprime_coe] at *; apply Nat.Coprime.pow; apply h #align pnat.coprime.pow PNat.Coprime.pow diff --git a/Mathlib/Data/Rat/Cast/CharZero.lean b/Mathlib/Data/Rat/Cast/CharZero.lean index a7ea66b826325..4be634e559ebc 100644 --- a/Mathlib/Data/Rat/Cast/CharZero.lean +++ b/Mathlib/Data/Rat/Cast/CharZero.lean @@ -121,7 +121,7 @@ theorem cast_mk (a b : ℤ) : (a /. b : α) = a / b := by #align rat.cast_mk Rat.cast_mk @[simp, norm_cast] -theorem cast_pow (q) (k : ℕ) : ((q : ℚ) ^ k : α) = (q : α) ^ k := +theorem cast_pow (q) (k : ℕ) : ((q ^ k : ℚ) : α) = (q : α) ^ k := (castHom α).map_pow q k #align rat.cast_pow Rat.cast_pow diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 17a3333557acb..743d222b58bb4 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -101,7 +101,7 @@ theorem Quotient.smul_mk [QuotientAction β H] (b : β) (a : α) : @[to_additive (attr := simp)] theorem Quotient.smul_coe [QuotientAction β H] (b : β) (a : α) : - b • (a : α ⧸ H) = (b • a : α ⧸ H) := + b • (a : α ⧸ H) = (↑(b • a) : α ⧸ H) := rfl #align mul_action.quotient.smul_coe MulAction.Quotient.smul_coe #align add_action.quotient.vadd_coe AddAction.Quotient.vadd_coe diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean index 370a8390d7d8d..4b9a8d2134463 100644 --- a/Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean +++ b/Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean @@ -115,14 +115,14 @@ instance : Monoid (SubMulAction R M) := { SubMulAction.semiGroup, SubMulAction.mulOneClass with } -theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), (p ^ n : Set M) = ((p : Set M) ^ n) +theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = ((p : Set M) ^ n) | 0, hn => (hn rfl).elim | 1, _ => by rw [pow_one, pow_one] | n + 2, _ => by rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero] #align sub_mul_action.coe_pow SubMulAction.coe_pow -theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, ((p : Set M) ^ n) ⊆ (p ^ n : Set M) +theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, ((p : Set M) ^ n) ⊆ ↑(p ^ n) | 0 => by rw [pow_zero, pow_zero] exact subset_coe_one diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean index f0c1d6d43154e..0465be825b237 100644 --- a/Mathlib/GroupTheory/Submonoid/Operations.lean +++ b/Mathlib/GroupTheory/Submonoid/Operations.lean @@ -560,7 +560,7 @@ attribute [to_additive existing nSMul] nPow @[to_additive (attr := simp, norm_cast)] theorem coe_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S) - (n : ℕ) : (x ^ n : M) = (x : M) ^ n := + (n : ℕ) : ↑(x ^ n) = (x : M) ^ n := rfl #align submonoid_class.coe_pow SubmonoidClass.coe_pow #align add_submonoid_class.coe_nsmul AddSubmonoidClass.coe_nsmul diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean index f48e08394faf8..2d4282a79658c 100644 --- a/Mathlib/LinearAlgebra/Alternating/Basic.lean +++ b/Mathlib/LinearAlgebra/Alternating/Basic.lean @@ -255,8 +255,7 @@ theorem smul_apply (c : S) (m : ι → M) : (c • f) m = c • f m := #align alternating_map.smul_apply AlternatingMap.smul_apply @[norm_cast] -theorem coe_smul (c : S) : (c • f : MultilinearMap R (fun _ : ι => M) N) = - c • (f : MultilinearMap R (fun _ : ι => M) N) := +theorem coe_smul (c : S) : ↑(c • f) = c • (f : MultilinearMap R (fun _ : ι => M) N) := rfl #align alternating_map.coe_smul AlternatingMap.coe_smul diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean index f722e92f77b3b..b730b3cb142d7 100644 --- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean @@ -326,7 +326,7 @@ total mass. -/ def normalize : ProbabilityMeasure Ω := if zero : μ.mass = 0 then ⟨Measure.dirac ‹Nonempty Ω›.some, Measure.dirac.isProbabilityMeasure⟩ else - { val := μ.mass⁻¹ • μ + { val := ↑(μ.mass⁻¹ • μ) property := by refine' ⟨_⟩ -- porting note: paying the price that this isn't `simp` lemma now. diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 8c8e522a65127..a4c58d159a44a 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -605,13 +605,13 @@ theorem smul_apply (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (c @[simp, norm_cast] theorem coe_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) : - (c • f : M₁ →ₛₗ[σ₁₂] M₂) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) := + ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) := rfl #align continuous_linear_map.coe_smul ContinuousLinearMap.coe_smul @[simp, norm_cast] theorem coe_smul' (c : S₂) (f : M₁ →SL[σ₁₂] M₂) : - (c • f : M₁ → M₂) = c • (f : M₁ → M₂) := + ↑(c • f) = c • (f : M₁ → M₂) := rfl #align continuous_linear_map.coe_smul' ContinuousLinearMap.coe_smul' From 738ad0b1a96ead61d11b270ccd006461d3eb7397 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 29 Oct 2023 12:17:45 -0700 Subject: [PATCH 04/10] mathlib fixes --- Mathlib/Algebra/GradedMonoid.lean | 4 +-- Mathlib/Algebra/GroupPower/NegOnePow.lean | 4 +-- Mathlib/Algebra/RingQuot.lean | 2 +- Mathlib/Analysis/Fourier/AddCircle.lean | 10 +++--- .../Fourier/RiemannLebesgueLemma.lean | 4 +-- .../Analysis/InnerProductSpace/Calculus.lean | 4 +-- .../Analysis/InnerProductSpace/Rayleigh.lean | 4 +-- .../Analysis/InnerProductSpace/TwoDim.lean | 2 +- Mathlib/Analysis/MellinTransform.lean | 4 +-- Mathlib/Analysis/NormedSpace/DualNumber.lean | 2 +- Mathlib/Analysis/NormedSpace/PiLp.lean | 2 +- Mathlib/Analysis/NormedSpace/ProdLp.lean | 5 +-- .../NormedSpace/QuaternionExponential.lean | 4 +-- Mathlib/Analysis/NormedSpace/Star/Matrix.lean | 2 +- Mathlib/Analysis/PSeries.lean | 9 +++-- .../SpecialFunctions/Gamma/Basic.lean | 2 +- .../Analysis/SpecialFunctions/Gamma/Beta.lean | 8 ++--- .../Analysis/SpecialFunctions/Integrals.lean | 18 +++++----- .../Analysis/SpecialFunctions/Pow/Deriv.lean | 6 ++-- .../Analysis/SpecialFunctions/Pow/NNReal.lean | 2 +- .../Analysis/SpecialFunctions/Stirling.lean | 4 +-- .../SpecialFunctions/Trigonometric/Angle.lean | 4 +-- .../Trigonometric/Bounds.lean | 2 +- .../Trigonometric/EulerSineProd.lean | 4 +-- Mathlib/Combinatorics/Additive/Behrend.lean | 20 +++++------ Mathlib/Data/PNat/Basic.lean | 2 +- Mathlib/FieldTheory/PrimitiveElement.lean | 2 +- Mathlib/FieldTheory/Subfield.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Polynomial.lean | 11 +++--- .../Covering/Differentiation.lean | 15 ++++---- Mathlib/MeasureTheory/Function/L2Space.lean | 3 +- .../Function/UniformIntegrable.lean | 6 ++-- Mathlib/MeasureTheory/Integral/Bochner.lean | 8 ++--- .../Measure/Haar/InnerProductSpace.lean | 5 ++- Mathlib/NumberTheory/Basic.lean | 2 +- Mathlib/NumberTheory/Bernoulli.lean | 3 +- Mathlib/NumberTheory/Bertrand.lean | 20 +++++------ Mathlib/NumberTheory/ClassNumber/Finite.lean | 3 +- .../NumberTheory/Cyclotomic/Discriminant.lean | 4 +-- .../Cyclotomic/PrimitiveRoots.lean | 6 ++-- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 2 +- .../LegendreSymbol/GaussEisensteinLemmas.lean | 2 +- .../LegendreSymbol/JacobiSymbol.lean | 2 +- .../Liouville/LiouvilleNumber.lean | 4 +-- .../ModularForms/JacobiTheta/Basic.lean | 14 ++++---- Mathlib/NumberTheory/NumberField/Units.lean | 4 +-- .../NumberTheory/Padics/PadicIntegers.lean | 3 +- Mathlib/NumberTheory/Padics/PadicVal.lean | 3 +- Mathlib/NumberTheory/Padics/RingHoms.lean | 2 +- Mathlib/NumberTheory/ZetaFunction.lean | 2 +- .../Zsqrtd/QuadraticReciprocity.lean | 2 +- Mathlib/Probability/Notation.lean | 3 +- Mathlib/Probability/StrongLaw.lean | 2 +- Mathlib/Probability/Variance.lean | 8 ++--- .../HomogeneousLocalization.lean | 2 +- Mathlib/RingTheory/RootsOfUnity/Basic.lean | 2 +- Mathlib/RingTheory/WittVector/Frobenius.lean | 2 +- .../WittVector/StructurePolynomial.lean | 3 +- Mathlib/SetTheory/Cardinal/Basic.lean | 22 ++++++------ Mathlib/SetTheory/Cardinal/Divisibility.lean | 3 +- Mathlib/SetTheory/Ordinal/Exponential.lean | 35 ++++++++++--------- Mathlib/SetTheory/Ordinal/Notation.lean | 26 +++++++------- Mathlib/SetTheory/Ordinal/Principal.lean | 4 +-- .../Topology/Algebra/Module/Cardinality.lean | 4 +-- .../Algebra/Nonarchimedean/AdicTopology.lean | 4 +-- .../MetricSpace/HausdorffDimension.lean | 2 +- test/positivity.lean | 2 +- 67 files changed, 195 insertions(+), 193 deletions(-) diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean index 5df53faf5eead..2342f2f95770e 100644 --- a/Mathlib/Algebra/GradedMonoid.lean +++ b/Mathlib/Algebra/GradedMonoid.lean @@ -320,8 +320,8 @@ section Monoid variable [AddMonoid ι] [GMonoid A] -instance : Pow (A 0) ℕ where - pow x n := @Eq.rec ι (n • (0:ι)) (fun a _ => A a) (GMonoid.gnpow n x) 0 (nsmul_zero n) +instance : NatPow (A 0) where + natPow x n := @Eq.rec ι (n • (0:ι)) (fun a _ => A a) (GMonoid.gnpow n x) 0 (nsmul_zero n) variable {A} diff --git a/Mathlib/Algebra/GroupPower/NegOnePow.lean b/Mathlib/Algebra/GroupPower/NegOnePow.lean index d53c1e0bf8040..c3207db4e6d2d 100644 --- a/Mathlib/Algebra/GroupPower/NegOnePow.lean +++ b/Mathlib/Algebra/GroupPower/NegOnePow.lean @@ -19,9 +19,9 @@ namespace Int /-- The map `ℤ → ℤ` which sends `n` to `(-1 : ℤˣ) ^ n`. -/ @[pp_dot] -def negOnePow (n : ℤ) : ℤ := (-1 : ℤˣ) ^ n +def negOnePow (n : ℤ) : ℤ := ↑((-1 : ℤˣ) ^ n) -lemma negOnePow_def (n : ℤ) : n.negOnePow = (-1 : ℤˣ) ^ n := rfl +lemma negOnePow_def (n : ℤ) : n.negOnePow = ↑((-1 : ℤˣ) ^ n) := rfl lemma negOnePow_add (n₁ n₂ : ℤ) : (n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow := by diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean index ea0f9967e3af1..d199723aad31a 100644 --- a/Mathlib/Algebra/RingQuot.lean +++ b/Mathlib/Algebra/RingQuot.lean @@ -218,7 +218,7 @@ instance : Add (RingQuot r) := instance : Mul (RingQuot r) := ⟨mul r⟩ -instance : Pow (RingQuot r) ℕ := +instance : NatPow (RingQuot r) := ⟨fun x n ↦ npow r n x⟩ instance {R : Type uR} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) := diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 01f27086663af..41f5f7a536106 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -146,12 +146,12 @@ section Monomials /-- The family of exponential monomials `fun x => exp (2 π i n x / T)`, parametrized by `n : ℤ` and considered as bundled continuous maps from `ℝ / ℤ • T` to `ℂ`. -/ def fourier (n : ℤ) : C(AddCircle T, ℂ) where - toFun x := toCircle (n • x) + toFun x := toCircle (n • x :) continuous_toFun := continuous_induced_dom.comp <| continuous_toCircle.comp <| continuous_zsmul _ #align fourier fourier @[simp] -theorem fourier_apply {n : ℤ} {x : AddCircle T} : fourier n x = toCircle (n • x) := +theorem fourier_apply {n : ℤ} {x : AddCircle T} : fourier n x = toCircle (n • x :) := rfl #align fourier_apply fourier_apply @@ -167,7 +167,7 @@ theorem fourier_coe_apply {n : ℤ} {x : ℝ} : @[simp] theorem fourier_coe_apply' {n : ℤ} {x : ℝ} : - toCircle (n • (x : AddCircle T)) = Complex.exp (2 * π * Complex.I * n * x / T) := by + toCircle (n • (x : AddCircle T) :) = Complex.exp (2 * π * Complex.I * n * x / T) := by rw [← fourier_apply]; exact fourier_coe_apply -- @[simp] -- Porting note: simp normal form is `fourier_zero'` @@ -212,7 +212,7 @@ theorem fourier_add {m n : ℤ} {x : AddCircle T} : fourier (m+n) x = fourier m @[simp] theorem fourier_add' {m n : ℤ} {x : AddCircle T} : - toCircle ((m + n) • x) = fourier m x * fourier n x := by + toCircle ((m + n) • x :) = fourier m x * fourier n x := by rw [← fourier_apply]; exact fourier_add theorem fourier_norm [Fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1 := by @@ -365,7 +365,7 @@ theorem fourierCoeff_eq_intervalIntegral (f : AddCircle T → E) (n : ℤ) (a : #align fourier_coeff_eq_interval_integral fourierCoeff_eq_intervalIntegral theorem fourierCoeff.const_smul (f : AddCircle T → E) (c : ℂ) (n : ℤ) : - fourierCoeff (c • f) n = c • fourierCoeff f n := by + fourierCoeff (c • f :) n = c • fourierCoeff f n := by simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul, smul_assoc, integral_smul] #align fourier_coeff.const_smul fourierCoeff.const_smul diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index 2ac9712a817d8..8774809388597 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -70,9 +70,7 @@ theorem fourier_integrand_integrable (w : V) : variable [CompleteSpace E] --- Porting note: binary operations appear not to work? --- local notation "i" => fun w => (1 / (2 * ‖w‖ ^ 2)) • w -local notation "i" => fun (w : V) => HDiv.hDiv (1 : ℝ) (HMul.hMul (2 : ℝ) (HPow.hPow ‖w‖ 2)) • w +local notation3 "i" => fun (w : V) => (1 / (2 * ‖w‖ ^ 2) : ℝ) • w /-- Shifting `f` by `(1 / (2 * ‖w‖ ^ 2)) • w` negates the integral in the Riemann-Lebesgue lemma. -/ theorem fourier_integral_half_period_translate {w : V} (hw : w ≠ 0) : diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean index d3cb193d705e5..edaac53116266 100644 --- a/Mathlib/Analysis/InnerProductSpace/Calculus.lean +++ b/Mathlib/Analysis/InnerProductSpace/Calculus.lean @@ -400,7 +400,7 @@ open Metric hiding mem_nhds_iff variable {n : ℕ∞} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] theorem LocalHomeomorph.contDiff_univUnitBall : ContDiff ℝ n (univUnitBall : E → E) := by - suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ from this.smul contDiff_id + suffices ContDiff ℝ n fun x : E => (1 + ‖x‖ ^ 2 : ℝ).sqrt⁻¹ from this.smul contDiff_id have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity refine' ContDiff.inv _ fun x => Real.sqrt_ne_zero'.mpr (h x) exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne' @@ -408,7 +408,7 @@ theorem LocalHomeomorph.contDiff_univUnitBall : ContDiff ℝ n (univUnitBall : E theorem LocalHomeomorph.contDiffOn_univUnitBall_symm : ContDiffOn ℝ n univUnitBall.symm (ball (0 : E) 1) := fun y hy ↦ by apply ContDiffAt.contDiffWithinAt - suffices ContDiffAt ℝ n (fun y : E => ((1 : ℝ) - ‖y‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id + suffices ContDiffAt ℝ n (fun y : E => (1 - ‖y‖ ^ 2 : ℝ).sqrt⁻¹) y from this.smul contDiffAt_id have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy refine' ContDiffAt.inv _ (Real.sqrt_ne_zero'.mpr h) diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean index b1c5701128299..d88886429c42b 100644 --- a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean +++ b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean @@ -240,7 +240,7 @@ namespace IsSymmetric /-- The supremum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial finite-dimensional vector space is an eigenvalue for that operator. -/ theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) : - HasEigenvalue T ↑(⨆ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2) := by + HasEigenvalue T ↑(⨆ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2 : ℝ) := by haveI := FiniteDimensional.proper_isROrC 𝕜 E let T' := hT.toSelfAdjoint obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0 @@ -260,7 +260,7 @@ theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) : /-- The infimum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial finite-dimensional vector space is an eigenvalue for that operator. -/ theorem hasEigenvalue_iInf_of_finiteDimensional (hT : T.IsSymmetric) : - HasEigenvalue T ↑(⨅ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2) := by + HasEigenvalue T ↑(⨅ x : { x : E // x ≠ 0 }, IsROrC.re ⟪T x, x⟫ / ‖(x : E)‖ ^ 2 : ℝ) := by haveI := FiniteDimensional.proper_isROrC 𝕜 E let T' := hT.toSelfAdjoint obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0 diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean index 76790944f522a..fa1516ea40c93 100644 --- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -525,7 +525,7 @@ theorem kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y) #align orientation.kahler_neg_orientation Orientation.kahler_neg_orientation theorem kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y := by - trans (↑(‖a‖ ^ 2) : ℂ) * o.kahler x y + trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x y · ext · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul] diff --git a/Mathlib/Analysis/MellinTransform.lean b/Mathlib/Analysis/MellinTransform.lean index a0d87486204b9..1aefad2b113a7 100644 --- a/Mathlib/Analysis/MellinTransform.lean +++ b/Mathlib/Analysis/MellinTransform.lean @@ -150,7 +150,7 @@ theorem mellin_comp_mul_left (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) : rw [Ne.def, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or] exact Or.inl ha.ne' rw [set_integral_congr measurableSet_Ioi this, integral_smul, - integral_comp_mul_left_Ioi (fun u ↦ ↑u ^ (s - 1) • f u) _ ha, + integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha, mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg, cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, abs_of_pos (inv_pos.mpr ha), ofReal_inv, mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')] @@ -386,7 +386,7 @@ theorem mellin_hasDerivAt_of_isBigO_rpow [CompleteSpace E] [NormedSpace ℂ E] { rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz' have h5 : IntegrableOn bound (Ioi 0) := by simp_rw [add_mul, mul_assoc] - suffices ∀ {j : ℝ} (hj : b < j) (hj' : j < a), + suffices ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t : ℝ => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume by refine' Integrable.add (this _ _) (this _ _) all_goals linarith diff --git a/Mathlib/Analysis/NormedSpace/DualNumber.lean b/Mathlib/Analysis/NormedSpace/DualNumber.lean index 76d8d8fe8257c..2c89f6dff9153 100644 --- a/Mathlib/Analysis/NormedSpace/DualNumber.lean +++ b/Mathlib/Analysis/NormedSpace/DualNumber.lean @@ -37,7 +37,7 @@ theorem exp_eps : exp 𝕜 (eps : DualNumber R) = 1 + eps := @[simp] theorem exp_smul_eps (r : R) : exp 𝕜 (r • eps : DualNumber R) = 1 + r • eps := by - rw [eps, ← inr_smul, exp_inr, Nat.cast_one] + rw [eps, ← inr_smul, exp_inr] #align dual_number.exp_smul_eps DualNumber.exp_smul_eps end DualNumber diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean index 879865cb60aca..2c2e65bce4c3d 100644 --- a/Mathlib/Analysis/NormedSpace/PiLp.lean +++ b/Mathlib/Analysis/NormedSpace/PiLp.lean @@ -571,7 +571,7 @@ theorem norm_eq_of_nat {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} #align pi_Lp.norm_eq_of_nat PiLp.norm_eq_of_nat theorem norm_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp 2 β) : - ‖x‖ = sqrt (∑ i : ι, ‖x i‖ ^ 2) := by + ‖x‖ = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2) := by rw [norm_eq_of_nat 2 (by norm_cast) _] -- Porting note: was `convert` rw [Real.sqrt_eq_rpow] norm_cast diff --git a/Mathlib/Analysis/NormedSpace/ProdLp.lean b/Mathlib/Analysis/NormedSpace/ProdLp.lean index d73bae35d0c9a..ca0e1df70eb64 100644 --- a/Mathlib/Analysis/NormedSpace/ProdLp.lean +++ b/Mathlib/Analysis/NormedSpace/ProdLp.lean @@ -432,7 +432,7 @@ theorem prod_antilipschitzWith_equiv_aux [PseudoEMetricSpace α] [PseudoEMetricS simp [edist] · refine ENNReal.rpow_le_rpow ?_ (le_of_lt pos) simp [edist] - _ = (2 : ℝ≥0) ^ (1 / p.toReal) * edist (WithLp.equiv p _ x) (WithLp.equiv p _ y) := by + _ = (2 ^ (1 / p.toReal) : ℝ≥0) * edist (WithLp.equiv p _ x) (WithLp.equiv p _ y) := by simp only [← two_mul, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel, ENNReal.rpow_one, ← ENNReal.coe_rpow_of_nonneg _ nonneg, coe_ofNat] @@ -630,7 +630,8 @@ theorem prod_nnnorm_eq_sup (f : WithLp ∞ (α × β)) : ‖f‖₊ = ‖f.fst ext norm_cast -theorem prod_norm_eq_of_L2 (x : WithLp 2 (α × β)) : ‖x‖ = sqrt (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) := by +theorem prod_norm_eq_of_L2 (x : WithLp 2 (α × β)) : + ‖x‖ = Real.sqrt (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) := by rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow] norm_cast diff --git a/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean b/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean index dfbb794b7804e..be010371557ef 100644 --- a/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean +++ b/Mathlib/Analysis/NormedSpace/QuaternionExponential.lean @@ -59,7 +59,7 @@ theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c s ext n : 1 letI k : ℝ := ↑(2 * n)! calc - k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]; norm_cast + k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2] _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_ _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_ · congr 1 @@ -75,11 +75,11 @@ theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c s calc k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ', pow_mul, hq2] - norm_cast _ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_ _ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_ · congr 1 rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul] + norm_cast · rw [smul_smul] congr 1 simp_rw [pow_succ', mul_div_assoc, div_div_cancel_left' hqn] diff --git a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean index cbda220cdd7ec..5480cdcb90ba5 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean @@ -39,7 +39,7 @@ theorem entry_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.uni use j simp only [eq_self_iff_true, Finset.mem_univ_val, and_self_iff, sq_eq_sq] -- The L2 norm of a row is a diagonal entry of U * Uᴴ - have diag_eq_norm_sum : (U * Uᴴ) i i = ∑ x : n, ‖U i x‖ ^ 2 := by + have diag_eq_norm_sum : (U * Uᴴ) i i = (∑ x : n, ‖U i x‖ ^ 2 : ℝ) := by simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, IsROrC.mul_conj, IsROrC.normSq_eq_def', IsROrC.ofReal_pow]; norm_cast -- The L2 norm of a row is a diagonal entry of U * Uᴴ, real part diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean index 6cd216a11ce1b..ad67f66ee16ed 100644 --- a/Mathlib/Analysis/PSeries.lean +++ b/Mathlib/Analysis/PSeries.lean @@ -74,8 +74,11 @@ theorem sum_condensed_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m exacts [add_le_add ihn this, (add_le_add_right n.one_le_two_pow _ : 1 + 1 ≤ 2 ^ n + 1), add_le_add_right (Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _] - have : ∀ k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1)) ≤ f k := fun k hk => - hf (n.one_le_two_pow.trans_lt <| (Nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1) + have : ∀ k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1)) ≤ f k := by + -- Note(kmill): was `fun k hk => ...` but `mem_Ico.mp hk` was elaborating with some + -- delayed assignment metavariables that weren't resolved in time. `intro` fixes this. + intro k hk + exact hf (n.one_le_two_pow.trans_lt <| (Nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1) (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2) convert sum_le_sum this simp [pow_succ, two_mul] @@ -310,7 +313,7 @@ theorem sum_Ioc_inv_sq_le_sub {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) : positivity #align sum_Ioc_inv_sq_le_sub sum_Ioc_inv_sq_le_sub -theorem sum_Ioo_inv_sq_le (k n : ℕ) : (∑ i in Ioo k n, ((i : α) ^ 2)⁻¹) ≤ 2 / (k + 1) := +theorem sum_Ioo_inv_sq_le (k n : ℕ) : (∑ i in Ioo k n, (i ^ 2 : α)⁻¹) ≤ 2 / (k + 1) := calc (∑ i in Ioo k n, ((i : α) ^ 2)⁻¹) ≤ ∑ i in Ioc k (max (k + 1) n), ((i : α) ^ 2)⁻¹ := by apply sum_le_sum_of_subset_of_nonneg diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index c2eb5253bcac3..c799a05737608 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -209,7 +209,7 @@ theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) intro x hx have d1 : HasDerivAt (fun y : ℝ => (-y).exp) (-(-x).exp) x := by simpa using (hasDerivAt_neg x).exp - have d2 : HasDerivAt (fun y : ℝ => ↑y ^ s) (s * x ^ (s - 1)) x := by + have d2 : HasDerivAt (fun y : ℝ => (y : ℂ) ^ s) (s * x ^ (s - 1)) x := by have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_ simpa only [mul_one] using t.comp_ofReal simpa only [id.def, ofReal_re, ofReal_im, Ne.def, eq_self_iff_true, not_true, or_false_iff, diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index 7076300ca475c..3698ae430b74b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -286,13 +286,13 @@ theorem GammaSeq_eq_approx_Gamma_integral {s : ℂ} (hs : 0 < re s) {n : ℕ} (h /-- The main techical lemma for `GammaSeq_tendsto_Gamma`, expressing the integral defining the Gamma function for `0 < re s` as the limit of a sequence of integrals over finite intervals. -/ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) : - Tendsto (fun n : ℕ => ∫ x : ℝ in (0)..n, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1)) atTop + Tendsto (fun n : ℕ => ∫ x : ℝ in (0)..n, ((1 - x / n) ^ n : ℝ) * (x : ℂ) ^ (s - 1)) atTop (𝓝 <| Gamma s) := by rw [Gamma_eq_integral hs] -- We apply dominated convergence to the following function, which we will show is uniformly -- bounded above by the Gamma integrand `exp (-x) * x ^ (re s - 1)`. let f : ℕ → ℝ → ℂ := fun n => - indicator (Ioc 0 (n : ℝ)) fun x : ℝ => ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) + indicator (Ioc 0 (n : ℝ)) fun x : ℝ => ((1 - x / n) ^ n : ℝ) * (x : ℂ) ^ (s - 1) -- integrability of f have f_ible : ∀ n : ℕ, Integrable (f n) (volume.restrict (Ioi 0)) := by intro n @@ -320,7 +320,7 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) : refine' (Tendsto.comp (continuous_ofReal.tendsto _) _).const_mul _ convert tendsto_one_plus_div_pow_exp (-x) using 1 ext1 n - rw [neg_div, ← sub_eq_add_neg]; norm_cast + rw [neg_div, ← sub_eq_add_neg] -- let `convert` identify the remaining goals convert tendsto_integral_of_dominated_convergence _ (fun n => (f_ible n).1) (Real.GammaIntegral_convergent hs) _ @@ -401,7 +401,7 @@ theorem GammaSeq_mul (z : ℂ) {n : ℕ} (hn : n ≠ 0) : rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib, Nat.cast_zero, add_zero, add_comm (1 - z) n, ← add_sub_assoc] have : ∀ j : ℕ, (z + ↑(j + 1)) * (↑1 - z + ↑j) = - ↑((j + 1) ^ 2) * (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2) := by + ((j + 1) ^ 2 :) * (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2) := by intro j push_cast have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean index 2cc20129d5021..4f52e49c8a07c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals.lean @@ -559,10 +559,9 @@ theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : t ≠ -1) : have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht apply integral_eq_sub_of_hasDerivAt · intro x _ - have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x) x := by + have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by convert (hasDerivAt_pow 2 (x : ℂ)).const_add 1 - · norm_cast - · simp + simp have g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z => z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z := by intro z hz @@ -571,7 +570,6 @@ theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : t ≠ -1) : field_simp ring convert (HasDerivAt.comp (↑x) (g _) f).comp_ofReal using 1 - · simp · field_simp; ring · exact_mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x) · apply Continuous.intervalIntegrable @@ -597,7 +595,6 @@ theorem integral_mul_rpow_one_add_sq {t : ℝ} (ht : t ≠ -1) : · rw [← intervalIntegral.integral_ofReal] congr with x : 1 rw [ofReal_mul, this x t] - norm_cast · simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)] push_cast; rfl · rw [← ofReal_one, ← ofReal_neg, Ne.def, ofReal_inj] @@ -753,8 +750,9 @@ theorem integral_sin_pow_mul_cos_pow_odd (m n : ℕ) : simp only [_root_.pow_zero, _root_.pow_succ', mul_assoc, pow_mul, one_mul] congr! 5 rw [← sq, ← sq, cos_sq'] - _ = ∫ u in sin a..sin b, u ^ m * (↑1 - u ^ 2) ^ n := - integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos hc + _ = ∫ u in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n := by + -- Note(kmill): Didn't need `by exact`, but elaboration order seems to matter here. + exact integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos hc #align integral_sin_pow_mul_cos_pow_odd integral_sin_pow_mul_cos_pow_odd /-- The integral of `sin x * cos x`, given in terms of sin². @@ -845,10 +843,10 @@ theorem integral_sin_sq_mul_cos_sq : /-! ### Integral of misc. functions -/ -theorem integral_sqrt_one_sub_sq : ∫ x in (-1 : ℝ)..1, sqrt ((1 : ℝ) - x ^ 2) = π / 2 := +theorem integral_sqrt_one_sub_sq : ∫ x in (-1 : ℝ)..1, sqrt (1 - x ^ 2 : ℝ) = π / 2 := calc - _ = ∫ x in sin (-(π / 2)).. sin (π / 2), sqrt (↑1 - x ^ 2) := by rw [sin_neg, sin_pi_div_two] - _ = ∫ x in (-(π / 2))..(π / 2), sqrt (↑1 - sin x ^ 2) * cos x := + _ = ∫ x in sin (-(π / 2)).. sin (π / 2), sqrt (1 - x ^ 2 : ℝ) := by rw [sin_neg, sin_pi_div_two] + _ = ∫ x in (-(π / 2))..(π / 2), sqrt (1 - sin x ^ 2 : ℝ) * cos x := (integral_comp_mul_deriv (fun x _ => hasDerivAt_sin x) continuousOn_cos (by continuity)).symm _ = ∫ x in (-(π / 2))..(π / 2), cos x ^ 2 := by diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean index fdc0edd04d244..41bded1ec1b11 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -236,9 +236,9 @@ theorem hasDerivAt_ofReal_cpow {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ -1 rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ), neg_one_mul] simp_rw [mul_neg, ← neg_mul, ← ofReal_neg] - suffices HasDerivAt (fun y : ℝ => ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by + suffices HasDerivAt (fun y : ℝ => (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by convert this.neg.mul_const _ using 1; ring - suffices HasDerivAt (fun y : ℝ => ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x) by + suffices HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x) by convert @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1 rw [real_smul, ofReal_neg 1, ofReal_one]; ring suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by @@ -329,7 +329,7 @@ lemma differentiableAt_rpow_const_of_ne (p : ℝ) {x : ℝ} (hx : x ≠ 0) : (hasStrictDerivAt_rpow_const_of_ne hx p).differentiableAt lemma differentiableOn_rpow_const (p : ℝ) : - DifferentiableOn ℝ (fun x => x ^ p) {0}ᶜ := + DifferentiableOn ℝ (fun x => (x : ℝ) ^ p) {0}ᶜ := fun _ hx => (Real.differentiableAt_rpow_const_of_ne p hx).differentiableWithinAt /-- This lemma says that `fun x => a ^ x` is strictly differentiable for `a < 0`. Note that these diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 33ac38cdd9b4a..8b1b355242171 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -440,7 +440,7 @@ theorem coe_rpow_of_nonneg (x : ℝ≥0) {y : ℝ} (h : 0 ≤ y) : (x : ℝ≥0 #align ennreal.coe_rpow_of_nonneg ENNReal.coe_rpow_of_nonneg theorem coe_rpow_def (x : ℝ≥0) (y : ℝ) : - (x : ℝ≥0∞) ^ y = if x = 0 ∧ y < 0 then ⊤ else (x ^ y : ℝ≥0∞) := + (x : ℝ≥0∞) ^ y = if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y) := rfl #align ennreal.coe_rpow_def ENNReal.coe_rpow_def diff --git a/Mathlib/Analysis/SpecialFunctions/Stirling.lean b/Mathlib/Analysis/SpecialFunctions/Stirling.lean index 1a94400789a53..83fd055c26252 100644 --- a/Mathlib/Analysis/SpecialFunctions/Stirling.lean +++ b/Mathlib/Analysis/SpecialFunctions/Stirling.lean @@ -75,10 +75,10 @@ theorem log_stirlingSeq_formula (n : ℕ) : `∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))` -/ theorem log_stirlingSeq_diff_hasSum (m : ℕ) : - HasSum (fun k : ℕ => ↑1 / (↑2 * ↑(k + 1) + ↑1) * (((1:ℝ)/(↑2 * ↑(m + 1) + ↑1)) ^ 2) ^ ↑(k + 1)) + HasSum (fun k : ℕ => ↑1 / (↑2 * ↑(k + 1) + ↑1) * (((1:ℝ)/(↑2 * (m + 1 :) + ↑1)) ^ 2) ^ ↑(k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))) := by change HasSum - ((fun b : ℕ => (1:ℝ) / ((2:ℝ) * b + (1:ℝ)) * (((1:ℝ) / (2 * ↑(m + 1) + 1)) ^ 2) ^ b) ∘ succ) _ + ((fun b : ℕ => (1:ℝ) / ((2:ℝ) * b + (1:ℝ)) * (((1:ℝ) / (2 * (m + 1 :) + 1)) ^ 2) ^ b) ∘ succ) _ refine' (hasSum_nat_add_iff (a := _ - _) -- Porting note: must give implicit arguments (f := (fun b : ℕ => ↑1 / (↑2 * b + ↑1) * (((1:ℝ) / (2 * ↑(m + 1) + 1)) ^ 2) ^ b)) 1).mpr _ convert (hasSum_log_one_add_inv <| diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean index b36f0f1b8c80a..0687a34849fa9 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean @@ -184,7 +184,7 @@ theorem two_zsmul_eq_iff {ψ θ : Angle} : (2 : ℤ) • ψ = (2 : ℤ) • θ -- Porting note: no `Int.natAbs_bit0` anymore have : Int.natAbs 2 = 2 := rfl rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero, - Fin.val_one, zero_smul, coe_zero, add_zero, one_smul, Int.cast_two, + Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two, mul_div_cancel_left (_ : ℝ) two_ne_zero] #align real.angle.two_zsmul_eq_iff Real.Angle.two_zsmul_eq_iff @@ -224,7 +224,7 @@ theorem neg_ne_self_iff {θ : Angle} : -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ π := #align real.angle.neg_ne_self_iff Real.Angle.neg_ne_self_iff theorem two_nsmul_eq_pi_iff {θ : Angle} : (2 : ℕ) • θ = π ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ) := by - have h : (π : Angle) = (2 : ℕ) • (π / 2 : ℝ) := by rw [two_nsmul, add_halves] + have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves] nth_rw 1 [h] rw [coe_nsmul, two_nsmul_eq_iff] -- Porting note: `congr` didn't simplify the goal of iff of `Or`s diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean index a48ff98741474..f14557d73a791 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean @@ -106,7 +106,7 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x := by apply lt_of_le_of_ne y.cos_sq_le_one rw [cos_sq'] simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne' - rwa [one_div, lt_inv, inv_one] + rwa [lt_inv, inv_one] · exact zero_lt_one simpa only [sq, mul_self_pos] using this.ne' have mono := Convex.strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean index 751fcf1076166..409c92704e6b2 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean @@ -333,8 +333,8 @@ theorem _root_.Real.tendsto_euler_sin_prod (x : ℝ) : · ext1 n rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.ofReal_mul_re] suffices - (∏ j : ℕ in Finset.range n, ((1 : ℂ) - (x : ℂ) ^ 2 / ((j : ℂ) + 1) ^ 2)) = - (∏ j : ℕ in Finset.range n, ((1 : ℝ) - x ^ 2 / ((j : ℝ) + 1) ^ 2) : ℝ) by + (∏ j : ℕ in Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℂ) = + (∏ j : ℕ in Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℝ) by rw [this, Complex.ofReal_re] rw [Complex.ofReal_prod] refine' Finset.prod_congr (by rfl) fun n _ => _ diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean index 7c21bed69936c..0e4a2fea317d7 100644 --- a/Mathlib/Combinatorics/Additive/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/Behrend.lean @@ -239,7 +239,7 @@ that we then optimize by tweaking the parameters. The (almost) optimal parameter theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 + 1), - (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) : ℝ) ≤ (sphere n d k).card := by + (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ (sphere n d k).card := by refine' exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => _) nonempty_range_succ _ · rw [mem_range, lt_succ_iff] exact sum_sq_le_of_mem_box hx @@ -248,14 +248,14 @@ theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 + exact (cast_add_one_pos _).ne' #align behrend.exists_large_sphere_aux Behrend.exists_large_sphere_aux -theorem exists_large_sphere (n d : ℕ) : ∃ k, (d ^ n / ↑(n * d ^ 2) : ℝ) ≤ (sphere n d k).card := by +theorem exists_large_sphere (n d : ℕ) : + ∃ k, ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ (sphere n d k).card := by obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d refine' ⟨k, _⟩ obtain rfl | hn := n.eq_zero_or_pos · simp obtain rfl | hd := d.eq_zero_or_pos · simp - rw [rpow_nat_cast, ← cast_pow] refine' (div_le_div_of_le_left _ _ _).trans hk · exact cast_nonneg _ · exact cast_add_one_pos _ @@ -268,16 +268,16 @@ theorem exists_large_sphere (n d : ℕ) : ∃ k, (d ^ n / ↑(n * d ^ 2) : ℝ) exact one_le_cast.2 hd #align behrend.exists_large_sphere Behrend.exists_large_sphere -theorem bound_aux' (n d : ℕ) : (d ^ n / ↑(n * d ^ 2) : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) := +theorem bound_aux' (n d : ℕ) : ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) := let ⟨_, h⟩ := exists_large_sphere n d h.trans <| cast_le.2 <| card_sphere_le_rothNumberNat _ _ _ #align behrend.bound_aux' Behrend.bound_aux' theorem bound_aux (hd : d ≠ 0) (hn : 2 ≤ n) : - (d ^ (n - 2) / n : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) := by + (d ^ (n - 2 :) / n : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) := by convert bound_aux' n d using 1 - rw [cast_mul, cast_pow, mul_comm, ← div_div, ← cast_two, ← cast_sub hn, rpow_nat_cast, - rpow_nat_cast, pow_sub₀ _ (cast_ne_zero.2 hd) hn, ← div_eq_mul_inv] + rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow] + rwa [cast_ne_zero] #align behrend.bound_aux Behrend.bound_aux open scoped Filter Topology @@ -432,7 +432,8 @@ theorem le_N (hN : 2 ≤ N) : (2 * dValue N - 1) ^ nValue N ≤ N := by apply this.trans suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N by exact_mod_cast this suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (1 / nValue N : ℝ) - · apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans + · rw [← rpow_nat_cast] + apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans rw [← rpow_mul (cast_nonneg _), one_div_mul_cancel, rpow_one] rw [cast_ne_zero] apply (nValue_pos hN).ne' @@ -487,7 +488,6 @@ theorem roth_lower_bound_explicit (hN : 4096 ≤ N) : have hn₂ : 2 ≤ n := two_le_nValue (hN.trans' <| by norm_num1) have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1) refine' ((bound_aux hd.ne' hn₂).trans <| cast_le.2 <| rothNumberNat.mono this).trans_lt' _ - conv_rhs => rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast] refine' (div_lt_div_of_lt hn <| pow_lt_pow_of_lt_left (bound hN) _ _).trans_le' _ · exact div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) (exp_pos _).le · exact tsub_pos_of_lt (three_le_nValue <| hN.trans' <| by norm_num1) @@ -521,7 +521,7 @@ theorem exp_four_lt : exp 4 < 64 := by theorem four_zero_nine_six_lt_exp_sixteen : 4096 < exp 16 := by rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by norm_num), show (4096 : ℝ) = 2 ^ 12 by norm_cast, - log_rpow zero_lt_two] + ← rpow_nat_cast, log_rpow zero_lt_two, cast_ofNat] have : 12 * (0.6931471808 : ℝ) < 16 := by norm_num linarith [log_two_lt_d9] #align behrend.four_zero_nine_six_lt_exp_sixteen Behrend.four_zero_nine_six_lt_exp_sixteen diff --git a/Mathlib/Data/PNat/Basic.lean b/Mathlib/Data/PNat/Basic.lean index f068e176455cb..c9e0b5b61d94a 100644 --- a/Mathlib/Data/PNat/Basic.lean +++ b/Mathlib/Data/PNat/Basic.lean @@ -270,7 +270,7 @@ theorem coe_bit1 (a : ℕ+) : ((bit1 a : ℕ+) : ℕ) = bit1 (a : ℕ) := end deprecated @[simp, norm_cast] -theorem pow_coe (m : ℕ+) (n : ℕ) : (m ^ n : ℕ) = (m : ℕ) ^ n := +theorem pow_coe (m : ℕ+) (n : ℕ) : ↑(m ^ n) = (m : ℕ) ^ n := rfl #align pnat.pow_coe PNat.pow_coe diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index eefb10b31c3bb..4a2ae8c2b03c4 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -61,7 +61,7 @@ theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α exact F⟮α.val⟯.zero_mem · obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx)) simp only at hn - rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0], Units.val_zpow_eq_zpow_val] + rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]] exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n #align field.exists_primitive_element_of_finite_top Field.exists_primitive_element_of_finite_top diff --git a/Mathlib/FieldTheory/Subfield.lean b/Mathlib/FieldTheory/Subfield.lean index d704a6749261e..dd2fd753336da 100644 --- a/Mathlib/FieldTheory/Subfield.lean +++ b/Mathlib/FieldTheory/Subfield.lean @@ -116,7 +116,7 @@ instance (s : S) : SMul ℚ s := ⟨fun a x => ⟨a • (x : K), rat_smul_mem s a x⟩⟩ @[simp] -theorem coe_rat_smul (s : S) (a : ℚ) (x : s) : (a • x : K) = a • (x : K) := +theorem coe_rat_smul (s : S) (a : ℚ) (x : s) : ↑(a • x) = a • (x : K) := rfl #align subfield_class.coe_rat_smul SubfieldClass.coe_rat_smul diff --git a/Mathlib/LinearAlgebra/Matrix/Polynomial.lean b/Mathlib/LinearAlgebra/Matrix/Polynomial.lean index 2aed45b3d6e9f..d2ead49e5afb0 100644 --- a/Mathlib/LinearAlgebra/Matrix/Polynomial.lean +++ b/Mathlib/LinearAlgebra/Matrix/Polynomial.lean @@ -37,7 +37,7 @@ open Polynomial Matrix Equiv.Perm namespace Polynomial theorem natDegree_det_X_add_C_le (A B : Matrix n n α) : - natDegree (det ((X : α[X]) • A.map C + B.map C)) ≤ Fintype.card n := by + natDegree (det ((X : α[X]) • A.map C + B.map C : Matrix n n α[X])) ≤ Fintype.card n := by rw [det_apply] refine' (natDegree_sum_le _ _).trans _ refine' Multiset.max_nat_le_of_forall_le _ _ _ @@ -45,13 +45,14 @@ theorem natDegree_det_X_add_C_le (A B : Matrix n n α) : Multiset.mem_map, exists_imp, Finset.mem_univ_val] intro g calc - natDegree (sign g • ∏ i : n, (X • A.map C + B.map C) (g i) i) ≤ - natDegree (∏ i : n, (X • A.map C + B.map C) (g i) i) := by + natDegree (sign g • ∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) ≤ + natDegree (∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) := by cases' Int.units_eq_one_or (sign g) with sg sg · rw [sg, one_smul] · rw [sg, Units.neg_smul, one_smul, natDegree_neg] - _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C) (g i) i) := - (natDegree_prod_le (Finset.univ : Finset n) fun i : n => (X • A.map C + B.map C) (g i) i) + _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C : Matrix n n α[X]) (g i) i) := + (natDegree_prod_le (Finset.univ : Finset n) fun i : n => + (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_) _ ≤ Fintype.card n := by simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ] dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul] diff --git a/Mathlib/MeasureTheory/Covering/Differentiation.lean b/Mathlib/MeasureTheory/Covering/Differentiation.lean index 69ad5fc5071f5..6757fff3105f4 100644 --- a/Mathlib/MeasureTheory/Covering/Differentiation.lean +++ b/Mathlib/MeasureTheory/Covering/Differentiation.lean @@ -549,13 +549,16 @@ theorem withDensity_le_mul {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht let ν := μ.withDensity (v.limRatioMeas hρ) let f := v.limRatioMeas hρ have f_meas : Measurable f := v.limRatioMeas_measurable hρ - have A : ν (s ∩ f ⁻¹' {0}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' {0}) := by + -- Note(kmill): smul elaborator when used for CoeFun fails to get CoeFun instance to trigger + -- unless you use the `(... :)` notation. Another fix is using `(2 : Nat)`, so this appears + -- to be an unpleasant interaction with default instances. + have A : ν (s ∩ f ⁻¹' {0}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {0}) := by apply le_trans _ (zero_le _) have M : MeasurableSet (s ∩ f ⁻¹' {0}) := hs.inter (f_meas (measurableSet_singleton _)) simp only [nonpos_iff_eq_zero, M, withDensity_apply, lintegral_eq_zero_iff f_meas] apply (ae_restrict_iff' M).2 exact eventually_of_forall fun x hx => hx.2 - have B : ν (s ∩ f ⁻¹' {∞}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' {∞}) := by + have B : ν (s ∩ f ⁻¹' {∞}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {∞}) := by apply le_trans (le_of_eq _) (zero_le _) apply withDensity_absolutelyContinuous μ _ rw [← nonpos_iff_eq_zero] @@ -563,7 +566,7 @@ theorem withDensity_le_mul {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht have C : ∀ n : ℤ, ν (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) ≤ - ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by + ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by intro n let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1)) have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico) @@ -595,10 +598,10 @@ theorem withDensity_le_mul {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht ∑' n : ℤ, ν (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := measure_eq_measure_preimage_add_measure_tsum_Ico_zpow ν f_meas hs ht _ ≤ - ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' {0}) + ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' {∞}) + - ∑' n : ℤ, ((t : ℝ≥0∞) ^ 2 • ρ) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := + ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {0}) + ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {∞}) + + ∑' n : ℤ, ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' Ico (t ^ n) (t ^ (n + 1))) := (add_le_add (add_le_add A B) (ENNReal.tsum_le_tsum C)) - _ = ((t : ℝ≥0∞) ^ 2 • ρ) s := + _ = ((t : ℝ≥0∞) ^ 2 • ρ :) s := (measure_eq_measure_preimage_add_measure_tsum_Ico_zpow ((t : ℝ≥0∞) ^ 2 • ρ) f_meas hs ht).symm #align vitali_family.with_density_le_mul VitaliFamily.withDensity_le_mul diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean index 2b4e7062e3bed..b880a7b3dba5c 100644 --- a/Mathlib/MeasureTheory/Function/L2Space.lean +++ b/Mathlib/MeasureTheory/Function/L2Space.lean @@ -131,7 +131,8 @@ theorem snorm_inner_lt_top (f g : α →₂[μ] E) : snorm (fun x : α => ⟪f x _ ≤ 2 * ‖f x‖ * ‖g x‖ := (mul_le_mul_of_nonneg_right (le_mul_of_one_le_left (norm_nonneg _) one_le_two) (norm_nonneg _)) - _ ≤ ‖‖f x‖ ^ 2 + ‖g x‖ ^ 2‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _) + -- TODO(kmill): the type ascription is getting around an elaboration error + _ ≤ ‖(‖f x‖ ^ 2 + ‖g x‖ ^ 2 : ℝ)‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _) refine' (snorm_mono_ae (ae_of_all _ h)).trans_lt ((snorm_add_le _ _ le_rfl).trans_lt _) · exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index 4dde1d4c5c1f5..7562e6e86dab7 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -950,11 +950,9 @@ theorem uniformIntegrable_average refine' le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * (n • C : ℝ≥0∞) ≤ C) · refine' (ENNReal.mul_le_mul_left hn ENNReal.coe_ne_top).2 _ conv_rhs => rw [← Finset.card_range n] - -- Porting note: Originally `exact Finset.sum_le_card_nsmul _ _ _ fun i hi => hC i` - convert Finset.sum_le_card_nsmul _ _ _ fun i _ => hC i - rw [ENNReal.coe_smul] + exact Finset.sum_le_card_nsmul _ _ _ fun i _ => hC i · simp only [ENNReal.coe_eq_zero, inv_eq_zero, Nat.cast_eq_zero] at hn - rw [ENNReal.coe_smul, nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_nat, + rw [nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_nat, ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul] all_goals simpa only [Ne.def, Nat.cast_eq_zero] diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index 4141e02592e0d..1d9af7c755905 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1324,17 +1324,13 @@ theorem Memℒp.snorm_eq_integral_rpow_norm {f : α → H} {p : ℝ≥0∞} (hp1 have A : ∫⁻ a : α, ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ a : α, ‖f a‖₊ ^ p.toReal ∂μ := by apply lintegral_congr intro x - rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm_eq_coe_nnnorm, - -- Porting note: Here and below `ENNReal.coe_rpow_of_nonneg` was not needed - ← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg] + rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm_eq_coe_nnnorm] simp only [snorm_eq_lintegral_rpow_nnnorm hp1 hp2, one_div] rw [integral_eq_lintegral_of_nonneg_ae]; rotate_left · exact eventually_of_forall fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _ · exact (hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable rw [A, ← ofReal_rpow_of_nonneg toReal_nonneg (inv_nonneg.2 toReal_nonneg), ofReal_toReal] - · simp_rw [← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg] - · simp_rw [← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg] - exact (lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top hp1 hp2 hf.2).ne + exact (lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top hp1 hp2 hf.2).ne #align measure_theory.mem_ℒp.snorm_eq_integral_rpow_norm MeasureTheory.Memℒp.snorm_eq_integral_rpow_norm end NormedAddCommGroup diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index 84c4d839314a1..60241aca84ee1 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean @@ -132,15 +132,14 @@ theorem volume_ball (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : exact lt_of_add_lt_of_nonneg_left h (sq_nonneg _) _ = volume (regionBetween (fun x => - Real.sqrt (1 - x ^ 2)) (fun x => Real.sqrt (1 - x ^ 2)) (Set.Ioc (-1) 1)) := by - simp_rw [regionBetween, Set.mem_Ioo, Set.mem_Ioc, ← Real.sq_lt, lt_tsub_iff_left, - Nat.cast_one] + simp_rw [regionBetween, Set.mem_Ioo, Set.mem_Ioc, ← Real.sq_lt, lt_tsub_iff_left] _ = ENNReal.ofReal ((2 : ℝ) * ∫ (a : ℝ) in Set.Ioc (-1) 1, Real.sqrt (1 - a ^ 2)) := by rw [volume_eq_prod, volume_regionBetween_eq_integral (Continuous.integrableOn_Ioc (by continuity)) (Continuous.integrableOn_Ioc (by continuity)) measurableSet_Ioc (fun _ _ => neg_le_self (Real.sqrt_nonneg _))] simp_rw [Pi.sub_apply, sub_neg_eq_add, ← two_mul, integral_mul_left] _ = NNReal.pi := by - rw [← intervalIntegral.integral_of_le (by norm_num : (-1 : ℝ) ≤ 1), Nat.cast_one, + rw [← intervalIntegral.integral_of_le (by norm_num : (-1 : ℝ) ≤ 1), integral_sqrt_one_sub_sq, two_mul, add_halves, ← NNReal.coe_real_pi, ofReal_coe_nnreal] diff --git a/Mathlib/NumberTheory/Basic.lean b/Mathlib/NumberTheory/Basic.lean index 3d5afd3fc4c1a..878ef79b3cf88 100644 --- a/Mathlib/NumberTheory/Basic.lean +++ b/Mathlib/NumberTheory/Basic.lean @@ -30,7 +30,7 @@ theorem dvd_sub_pow_of_dvd_sub {R : Type*} [CommRing R] {p : ℕ} {a b : R} (h : (k : ℕ) : (p ^ (k + 1) : R) ∣ a ^ p ^ k - b ^ p ^ k := by induction' k with k ih · rwa [pow_one, pow_zero, pow_one, pow_one] - rw [pow_succ' p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ, Nat.cast_mul] + rw [pow_succ' p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ] refine' mul_dvd_mul _ ih let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)}) have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton] diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 8de2a7d4d5ae6..73259be69f824 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -356,9 +356,8 @@ theorem sum_range_pow (n p : ℕ) : -- key step: a chain of equalities of power series -- porting note: altered proof slightly rw [← mul_right_inj' hexp, mul_comm] - simp only [← cast_pow] rw [←exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one, - bernoulliPowerSeries, mul_right_comm] + bernoulliPowerSeries, mul_right_comm] simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false] refine' Eq.trans (mul_eq_mul_right_iff.mpr _) (Eq.trans h_cauchy _) · left diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean index 48ee97fc0d7b5..5f5c16c57c6b8 100644 --- a/Mathlib/NumberTheory/Bertrand.lean +++ b/Mathlib/NumberTheory/Bertrand.lean @@ -99,17 +99,15 @@ theorem real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) : · have : sqrt (2 * 512) = 32 := (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1) rw [hf, log_nonpos_iff (hf' _ _), this, div_le_one] <;> norm_num1 - have : (512 : ℝ) = 2 ^ (9 : ℕ) - · rw [rpow_nat_cast 2 9]; norm_num1 - conv_lhs => rw [this] - have : (1024 : ℝ) = 2 ^ (10 : ℕ) - · rw [rpow_nat_cast 2 10]; norm_num1 - rw [this, ← rpow_mul, ← rpow_add] <;> norm_num1 - have : (4 : ℝ) = 2 ^ (2 : ℕ) - · rw [rpow_nat_cast 2 2]; norm_num1 - rw [this, ← rpow_mul] <;> norm_num1 - apply rpow_le_rpow_of_exponent_le <;> norm_num1 - apply rpow_pos_of_pos four_pos + · conv in 512 => equals 2 ^ 9 => norm_num1 + conv in 1024 => equals 2 ^ 10 => norm_num1 + conv in 32 => rw [← Nat.cast_ofNat] + rw [rpow_nat_cast, ← pow_mul, ← pow_add] + conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1 + rw [← rpow_mul, ← rpow_nat_cast] + apply rpow_le_rpow_of_exponent_le + all_goals norm_num1 + · apply rpow_pos_of_pos four_pos #align bertrand.real_main_inequality Bertrand.real_main_inequality end Bertrand diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index abae019871eaf..23230153b6804 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -223,7 +223,8 @@ theorem exists_mem_finsetApprox (a : S) {b} (hb : b ≠ (0 : R)) : have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty set ε : ℝ := normBound abv bS ^ (-1 / Fintype.card ι : ℝ) with ε_eq have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _ - have ε_le : (normBound abv bS : ℝ) * (abv b • ε) ^ Fintype.card ι ≤ abv b ^ Fintype.card ι := by + have ε_le : (normBound abv bS : ℝ) * (abv b • ε) ^ (Fintype.card ι : ℝ) + ≤ abv b ^ (Fintype.card ι : ℝ) := by have := normBound_pos abv bS have := abv.nonneg b rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel, rpow_neg_one, diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index 4b2a572e75008..1fb9153145d42 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -90,7 +90,7 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos, Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow, - pow_mul, hpo.pow.neg_one_pow]; · norm_cast + pow_mul, hpo.pow.neg_one_pow] refine' Nat.Even.sub_odd _ (even_two_mul _) odd_one rw [mul_left_comm, ← ha] exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt) @@ -201,7 +201,7 @@ theorem discr_odd_prime [IsCyclotomicExtension {p} K L] [hp : Fact (p : ℕ).Pri have : IsCyclotomicExtension {p ^ (0 + 1)} K L := by rw [zero_add, pow_one] infer_instance - have hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1)) := by simpa using hζ + have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1) :) := by simpa using hζ convert discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2 · rw [zero_add, pow_one, totient_prime hp.out] · rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub] diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index b0fd00ba38d07..25c30b810aa92 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -412,8 +412,8 @@ then the norm of `ζ - 1` is `p`. -/ theorem sub_one_norm_prime [hpri : Fact (p : ℕ).Prime] [hcyc : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (cyclotomic p K)) (h : p ≠ 2) : norm K (ζ - 1) = p := by - replace hirr : Irreducible (cyclotomic (↑(p ^ (0 + 1)) : ℕ) K) := by simp [hirr] - replace hζ : IsPrimitiveRoot ζ (↑(p ^ (0 + 1)) : ℕ) := by simp [hζ] + replace hirr : Irreducible (cyclotomic (p ^ (0 + 1) : ℕ) K) := by simp [hirr] + replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1) : ℕ) := by simp [hζ] haveI : IsCyclotomicExtension {p ^ (0 + 1)} K L := by simp [hcyc] simpa using sub_one_norm_prime_ne_two hζ hirr h #align is_primitive_root.sub_one_norm_prime IsPrimitiveRoot.sub_one_norm_prime @@ -451,7 +451,7 @@ theorem sub_one_norm_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 -- Porting note: `simpa using hirr` was `simp [hirr]`_ replace hirr : Irreducible (cyclotomic ((2 : ℕ+) ^ k : ℕ+) K) := by simpa using hirr -- Porting note: `simpa using hζ` was `simp [hζ]`_ - replace hζ : IsPrimitiveRoot ζ ((2 : ℕ+) ^ k) := by simpa using hζ + replace hζ : IsPrimitiveRoot ζ (2 ^ k : ℕ+) := by simpa using hζ obtain ⟨k₁, hk₁⟩ := exists_eq_succ_of_ne_zero (lt_of_lt_of_le zero_lt_two hk).ne.symm -- Porting note: the proof is slightly different because of coercions. simpa [hk₁, show ((2 : ℕ+) : ℕ) = 2 from rfl] using sub_one_norm_eq_eval_cyclotomic hζ this hirr diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index ec0cadec1d3cf..2adda0bdfaece 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -89,7 +89,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExt replace H := Subalgebra.smul_mem _ H u.inv -- Porting note: the proof is slightly different because of coercions. rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul, - Units.inv_mul, Int.cast_one, one_mul, PNat.pow_coe, Nat.cast_pow, smul_def, map_pow] at H + Units.inv_mul, Int.cast_one, one_mul, smul_def, map_pow] at H cases k · haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl have : x ∈ (⊥ : Subalgebra ℚ K) := by diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index ffc5aa0a931b5..5be06f3e6cced 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -93,7 +93,7 @@ private theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ} theorem gauss_lemma_aux (p : ℕ) [hp : Fact p.Prime] {a : ℤ} (hap : (a : ZMod p) ≠ 0) : (↑a ^ (p / 2) : ZMod p) = - (-1) ^ ((Ico 1 (p / 2).succ).filter fun x : ℕ => p / 2 < (a * x : ZMod p).val).card := + ((-1) ^ ((Ico 1 (p / 2).succ).filter fun x : ℕ => p / 2 < (a * x : ZMod p).val).card :) := (mul_left_inj' (show ((p / 2)! : ZMod p) ≠ 0 by rw [Ne.def, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le] exact Nat.div_lt_self hp.1.pos (by decide))).1 <| by diff --git a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean index 7b15dceee2531..04552a4060b64 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean @@ -480,7 +480,7 @@ theorem mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)] · rw [mod_left ↑(b % _), mod_left b, Int.coe_nat_mod, Int.emod_emod_of_dvd b] simp only [ha₂, Nat.cast_mul, ← mul_assoc] - exact dvd_mul_left (a' : ℤ) (↑4 * ↑(2 ^ e)) + apply dvd_mul_left -- porting note: In mathlib3, it was written `cases' e`. In Lean 4, this resulted in the choice -- of a name other than e (for the case distinction of line 482) so we indicate the name -- to use explicitly. diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean b/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean index 115358469645a..0c1230384b3c6 100644 --- a/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean +++ b/Mathlib/NumberTheory/Liouville/LiouvilleNumber.lean @@ -172,7 +172,7 @@ theorem remainder_lt (n : ℕ) {m : ℝ} (m2 : 2 ≤ m) : remainder m n < 1 / (m /-- The sum of the `k` initial terms of the Liouville number to base `m` is a ratio of natural numbers where the denominator is `m ^ k!`. -/ theorem partialSum_eq_rat {m : ℕ} (hm : 0 < m) (k : ℕ) : - ∃ p : ℕ, partialSum m k = p / (m ^ k ! : ℝ) := by + ∃ p : ℕ, partialSum m k = p / ((m ^ k ! :) : ℝ) := by induction' k with k h · exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]⟩ @@ -196,7 +196,7 @@ theorem liouville_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Liouville (liouvill intro n -- the first `n` terms sum to `p / m ^ k!` rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩ - refine' ⟨p, m ^ n !, by rw [Nat.cast_pow]; exact one_lt_pow mZ1 n.factorial_ne_zero, _⟩ + refine' ⟨p, m ^ n !, one_lt_pow mZ1 n.factorial_ne_zero, _⟩ push_cast rw [Nat.cast_pow] at hp -- separate out the sum of the first `n` terms and the rest diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean index f01c50e9f5070..fbfb973efdf0c 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean @@ -37,13 +37,13 @@ theorem norm_exp_mul_sq_le {z : ℂ} (hz : 0 < z.im) (n : ℤ) : have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz) refine' (le_of_eq _).trans (_ : y ^ n ^ 2 ≤ _) · rw [Complex.norm_eq_abs, Complex.abs_exp] - have : (↑π * I * (n : ℂ) ^ 2 * z).re = -π * z.im * (n : ℝ) ^ 2 := by - rw [(by push_cast; ring : ↑π * I * (n : ℂ) ^ 2 * z = ↑(π * (n : ℝ) ^ 2) * (z * I)), + have : (π * I * n ^ 2 * z : ℂ).re = -π * z.im * (n : ℝ) ^ 2 := by + rw [(by push_cast; ring : (π * I * n ^ 2 * z : ℂ) = (π * n ^ 2 : ℝ) * (z * I)), ofReal_mul_re, mul_I_re] ring obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n) rw [this, exp_mul, ← Int.cast_pow, rpow_int_cast, hm, zpow_ofNat] - · have : n ^ 2 = ↑(n.natAbs ^ 2) := by rw [Nat.cast_pow, Int.natAbs_sq] + · have : n ^ 2 = (n.natAbs ^ 2 :) := by rw [Nat.cast_pow, Int.natAbs_sq] rw [this, zpow_ofNat] exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self) #align norm_exp_mul_sq_le norm_exp_mul_sq_le @@ -70,13 +70,13 @@ theorem summable_exp_mul_sq {z : ℂ} (hz : 0 < z.im) : theorem jacobiTheta_two_add (z : ℂ) : jacobiTheta (2 + z) = jacobiTheta z := by refine' tsum_congr fun n => _ - suffices cexp (↑π * I * (n : ℂ) ^ 2 * 2) = 1 by rw [mul_add, Complex.exp_add, this, one_mul] - rw [(by push_cast; ring : ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * π * I)), Complex.exp_int_mul, + suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, one_mul] + rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), Complex.exp_int_mul, Complex.exp_two_pi_mul_I, one_zpow] #align jacobi_theta_two_add jacobiTheta_two_add -theorem jacobiTheta_T_sq_smul (τ : ℍ) : jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta τ := by - suffices ↑(ModularGroup.T ^ 2 • τ) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add] +theorem jacobiTheta_T_sq_smul (τ : ℍ) : jacobiTheta (ModularGroup.T ^ 2 • τ :) = jacobiTheta τ := by + suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add] have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd] norm_cast diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index 6506641b724bd..251efdc6eec91 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -88,10 +88,10 @@ variable {K} theorem coe_mul (x y : (𝓞 K)ˣ) : ((x * y : (𝓞 K)ˣ) : K) = (x : K) * (y : K) := rfl -theorem coe_pow (x : (𝓞 K)ˣ) (n : ℕ) : (x ^ n : K) = (x : K) ^ n := by +theorem coe_pow (x : (𝓞 K)ˣ) (n : ℕ) : (↑(x ^ n) : K) = (x : K) ^ n := by rw [← SubmonoidClass.coe_pow, ← val_pow_eq_pow_val] -theorem coe_zpow (x : (𝓞 K)ˣ) (n : ℤ) : (x ^ n : K) = (x : K) ^ n := by +theorem coe_zpow (x : (𝓞 K)ˣ) (n : ℤ) : (↑(x ^ n) : K) = (x : K) ^ n := by change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _ exact map_zpow _ x n diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index ba8e87ace530f..d940299d4586f 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -357,7 +357,8 @@ theorem norm_int_lt_one_iff_dvd (k : ℤ) : ‖(k : ℤ_[p])‖ < 1 ↔ (p : ℤ theorem norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : ‖(k : ℤ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k := - suffices ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ ↑(p ^ n) ∣ k by simpa [norm_int_cast_eq_padic_norm] + suffices ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k by + simpa [norm_int_cast_eq_padic_norm] padicNormE.norm_int_le_pow_iff_dvd _ _ #align padic_int.norm_int_le_pow_iff_dvd PadicInt.norm_int_le_pow_iff_dvd diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean index 703c9a3dd3719..8227fd8184cd4 100644 --- a/Mathlib/NumberTheory/Padics/PadicVal.lean +++ b/Mathlib/NumberTheory/Padics/PadicVal.lean @@ -607,7 +607,8 @@ lemma Nat.log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ padicVa rw [← lt_add_one_iff, ← mul_one (2 ^ _)] at h1 rw [← add_one_le_iff, pow_succ] at h2 refine' not_dvd_of_between_consec_multiples h1 (lt_of_le_of_ne' h2 _) pow_padicValNat_dvd - exact pow_succ_padicValNat_not_dvd n.succ_ne_zero ∘ dvd_of_eq + -- TODO(kmill): Why is this `p := 2` necessary? + exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq lemma Nat.max_log_padicValNat_succ_eq_log_succ (n : ℕ) : max (log 2 n) (padicValNat 2 (n + 1)) = log 2 (n + 1) := by diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean index c5980b3b24eea..36b70e84c6afc 100644 --- a/Mathlib/NumberTheory/Padics/RingHoms.lean +++ b/Mathlib/NumberTheory/Padics/RingHoms.lean @@ -146,7 +146,7 @@ theorem zmod_congr_of_sub_mem_span_aux (n : ℕ) (x : ℤ_[p]) (a b : ℤ) rw [← dvd_neg, neg_sub] at ha have := dvd_add ha hb rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ← - Int.cast_sub, pow_p_dvd_int_iff, Nat.cast_pow] at this + Int.cast_sub, pow_p_dvd_int_iff] at this #align padic_int.zmod_congr_of_sub_mem_span_aux PadicInt.zmod_congr_of_sub_mem_span_aux theorem zmod_congr_of_sub_mem_span (n : ℕ) (x : ℤ_[p]) (a b : ℕ) diff --git a/Mathlib/NumberTheory/ZetaFunction.lean b/Mathlib/NumberTheory/ZetaFunction.lean index c4a8e637a4079..925f311c52e95 100644 --- a/Mathlib/NumberTheory/ZetaFunction.lean +++ b/Mathlib/NumberTheory/ZetaFunction.lean @@ -491,7 +491,7 @@ theorem integral_cpow_mul_exp_neg_pi_mul_sq {s : ℂ} (hs : 0 < s.re) (n : ℕ) conv_rhs => congr rw [← smul_eq_mul, ← mellin_comp_mul_left _ _ pi_pos] - have : 1 / ((n : ℂ) + 1) ^ (2 * s) = (((n : ℝ) + 1) ^ (2 : ℝ) : ℂ) ^ (-s) := by + have : 1 / ((n : ℂ) + 1) ^ (2 * s) = (((n + 1) ^ (2 : ℝ) : ℝ) : ℂ) ^ (-s) := by rw [(by norm_num : (n : ℂ) + 1 = ↑((n : ℝ) + 1)), (by norm_num : 2 * s = ↑(2 : ℝ) * s), cpow_mul_ofReal_nonneg, one_div, cpow_neg] rw [← Nat.cast_succ] diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean index 25e3a6ae228d8..403f40dba084b 100644 --- a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean +++ b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean @@ -87,7 +87,7 @@ theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact p.Prime] (h irreducible_iff_prime.1 <| by_contradiction fun hpi => let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi - have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ p := by + have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ ↑p := by erw [← ZMod.nat_cast_mod p 4, hp3]; exact by decide this a b (hab ▸ by simp) #align gaussian_int.prime_of_nat_prime_of_mod_four_eq_three GaussianInt.prime_of_nat_prime_of_mod_four_eq_three diff --git a/Mathlib/Probability/Notation.lean b/Mathlib/Probability/Notation.lean index 63beed340bc7b..596ebcc961833 100644 --- a/Mathlib/Probability/Notation.lean +++ b/Mathlib/Probability/Notation.lean @@ -38,10 +38,11 @@ open scoped MeasureTheory scoped[ProbabilityTheory] notation "𝔼[" X "|" m "]" => MeasureTheory.condexp m MeasureTheory.MeasureSpace.volume X +-- Note(kmill): this notation tends to lead to ambiguity with GetElem notation. set_option quotPrecheck false in scoped[ProbabilityTheory] notation P "[" X "]" => ∫ x, ↑(X x) ∂P -scoped[ProbabilityTheory] notation "𝔼[" X "]" => ∫ a, X a +scoped[ProbabilityTheory] notation "𝔼[" X "]" => ∫ a, (X : _ → _) a scoped[ProbabilityTheory] notation P "⟦" s "|" m "⟧" => MeasureTheory.condexp m P (Set.indicator s fun ω => (1 : ℝ)) diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean index 5c375c2d228f9..2cd01ce9b2b7b 100644 --- a/Mathlib/Probability/StrongLaw.lean +++ b/Mathlib/Probability/StrongLaw.lean @@ -364,7 +364,7 @@ theorem sum_variance_truncation_le {X : Ω → ℝ} (hint : Integrable X) (hnonn simp only [hij, mem_sigma, mem_range, and_self_iff] · rintro ⟨i, j⟩ hij; rfl · rintro ⟨i, j⟩ hij; rfl - _ ≤ ∑ k in range K, ↑2 / (k + ↑1) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by + _ ≤ ∑ k in range K, 2 / (k + 1 : ℝ) * ∫ x in k..(k + 1 : ℕ), x ^ 2 ∂ρ := by apply sum_le_sum fun k _ => ?_ refine' mul_le_mul_of_nonneg_right (sum_Ioo_inv_sq_le _ _) _ refine' intervalIntegral.integral_nonneg_of_forall _ fun u => sq_nonneg _ diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean index 64c0ec5432091..41974ed462f84 100644 --- a/Mathlib/Probability/Variance.lean +++ b/Mathlib/Probability/Variance.lean @@ -114,7 +114,7 @@ theorem evariance_eq_lintegral_ofReal (X : Ω → ℝ) (μ : Measure Ω) : #align probability_theory.evariance_eq_lintegral_of_real ProbabilityTheory.evariance_eq_lintegral_ofReal theorem _root_.MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero (hX : Memℒp X 2 μ) - (hXint : μ[X] = 0) : variance X μ = μ[X ^ 2] := by + (hXint : μ[X] = 0) : variance X μ = μ[X ^ (2 : Nat)] := by rw [variance, evariance_eq_lintegral_ofReal, ← ofReal_integral_eq_lintegral_ofReal, ENNReal.toReal_ofReal] <;> simp_rw [hXint, sub_zero] @@ -127,7 +127,7 @@ theorem _root_.MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero (hX : Mem #align measure_theory.mem_ℒp.variance_eq_of_integral_eq_zero MeasureTheory.Memℒp.variance_eq_of_integral_eq_zero theorem _root_.MeasureTheory.Memℒp.variance_eq [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : - variance X μ = μ[(X - fun _ => μ[X]) ^ 2] := by + variance X μ = μ[(X - fun _ => μ[X] :) ^ (2 : Nat)] := by rw [variance, evariance_eq_lintegral_ofReal, ← ofReal_integral_eq_lintegral_ofReal, ENNReal.toReal_ofReal] · rfl @@ -241,7 +241,7 @@ theorem variance_le_expectation_sq [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → #align probability_theory.variance_le_expectation_sq ProbabilityTheory.variance_le_expectation_sq theorem evariance_def' [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → ℝ} (hX : AEStronglyMeasurable X ℙ) : - eVar[X] = (∫⁻ ω, ‖X ω‖₊ ^ 2) - ENNReal.ofReal (𝔼[X] ^ 2) := by + eVar[X] = (∫⁻ ω, (‖X ω‖₊ ^ 2 :)) - ENNReal.ofReal (𝔼[X] ^ 2) := by by_cases hℒ : Memℒp X 2 · rw [← hℒ.ofReal_variance_eq, variance_def' hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)] congr @@ -285,7 +285,7 @@ theorem meas_ge_le_variance_div_sq [@IsFiniteMeasure Ω _ ℙ] {X : Ω → ℝ} rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero _ hc.ne.symm), hX.ofReal_variance_eq] convert @meas_ge_le_evariance_div_sq _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1 · simp only [Real.coe_toNNReal', max_le_iff, abs_nonneg, and_true_iff] - · rw [ENNReal.ofReal_pow hc.le, ENNReal.coe_pow] + · rw [ENNReal.ofReal_pow hc.le] rfl #align probability_theory.meas_ge_le_variance_div_sq ProbabilityTheory.meas_ge_le_variance_div_sq diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean index 08330c9a3773d..25b8320fc8529 100644 --- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean +++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean @@ -342,7 +342,7 @@ instance : SMul α (HomogeneousLocalization 𝒜 x) where smul m := Quotient.map' (m • ·) fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) => by change Localization.mk _ _ = Localization.mk _ _ simp only [num_smul, den_smul] - convert congr_arg (fun z : at x => m • z) h <;> rw [Localization.smul_mk] <;> rfl + convert congr_arg (fun z : at x => m • z) h <;> rw [Localization.smul_mk] @[simp] theorem smul_val (y : HomogeneousLocalization 𝒜 x) (n : α) : (n • y).val = n • y.val := by diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index de71cc5cfb363..a9b2580bb36f6 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -129,7 +129,7 @@ theorem map_rootsOfUnity (f : Mˣ →* Nˣ) (k : ℕ+) : (rootsOfUnity k M).map @[norm_cast] theorem rootsOfUnity.coe_pow [CommMonoid R] (ζ : rootsOfUnity k R) (m : ℕ) : - ((ζ ^ m : Rˣ) : R) = ((ζ : Rˣ) : R) ^ m := by + (((ζ ^ m :) : Rˣ) : R) = ((ζ : Rˣ) : R) ^ m := by rw [Subgroup.coe_pow, Units.val_pow_eq_pow_val] #align roots_of_unity.coe_pow rootsOfUnity.coe_pow diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean index 90834dfcb9c96..953bcf4889262 100644 --- a/Mathlib/RingTheory/WittVector/Frobenius.lean +++ b/Mathlib/RingTheory/WittVector/Frobenius.lean @@ -191,7 +191,7 @@ theorem map_frobeniusPoly (n : ℕ) : have aux : ∀ k : ℕ, (p : ℚ)^ k ≠ 0 := by intro; apply pow_ne_zero; exact_mod_cast hp.1.ne_zero simpa [aux, -one_div, field_simps] using this.symm - rw [mul_comm _ (p : ℚ), mul_assoc, Nat.cast_pow, mul_assoc, ← pow_add, + rw [mul_comm _ (p : ℚ), mul_assoc, mul_assoc, ← pow_add, map_frobeniusPoly.key₂ p hi.le hj, Nat.cast_mul, Nat.cast_pow] ring #align witt_vector.map_frobenius_poly WittVector.map_frobeniusPoly diff --git a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean index 6ee1ade278846..0419307be00cb 100644 --- a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean +++ b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean @@ -232,7 +232,7 @@ theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx m < n → map (Int.castRingHom ℚ) (wittStructureInt p Φ m) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) m) : - (C (p ^ n : ℤ) : MvPolynomial (idx × ℕ) ℤ) ∣ + (C ((p ^ n :) : ℤ) : MvPolynomial (idx × ℕ) ℤ) ∣ bind₁ (fun b : idx => rename (fun i => (b, i)) (wittPolynomial p ℤ n)) Φ - ∑ i in range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i) := by cases' n with n @@ -262,7 +262,6 @@ theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k) rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ, ← tsub_add_eq_add_tsub hk]] rw [pow_mul] - rw [← Nat.cast_pow] -- Porting note: added -- the machine! apply dvd_sub_pow_of_dvd_sub rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow, diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index bda7d41c768df..be95232324011 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -493,7 +493,7 @@ local infixr:0 "^'" => @HPow.hPow Cardinal Cardinal Cardinal.instPowCardinal -- -- mathport name: cardinal.pow.nat local infixr:80 " ^ℕ " => @HPow.hPow Cardinal ℕ Cardinal instHPow -theorem power_def (α β) : #α ^ #β = #(β → α) := +theorem power_def (α β : Type u) : #α ^ #β = #(β → α) := rfl #align cardinal.power_def Cardinal.power_def @@ -508,12 +508,12 @@ theorem lift_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = ((lift.{v} a) ^ (li #align cardinal.lift_power Cardinal.lift_power @[simp] -theorem power_zero {a : Cardinal} : (a ^ 0) = 1 := +theorem power_zero {a : Cardinal} : (a ^ (0 : Cardinal)) = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.power_zero Cardinal.power_zero @[simp] -theorem power_one {a : Cardinal.{u}} : (a ^ 1) = a := +theorem power_one {a : Cardinal.{u}} : (a ^ (1 : Cardinal)) = a := inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α) #align cardinal.power_one Cardinal.power_one @@ -538,9 +538,9 @@ instance commSemiring : CommSemiring Cardinal.{u} where mul_comm := mul_comm' left_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodSumDistrib α β γ right_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumProdDistrib α β γ - npow n c := c^n + npow n c := c ^ (n : Cardinal) npow_zero := @power_zero - npow_succ n c := show (c ^ (n + 1 : ℕ)) = c * (c ^ n) + npow_succ n c := show (c ^ ((n + 1 : ℕ) : Cardinal)) = c * (c ^ (n : Cardinal)) by rw [Cardinal.cast_succ, power_add, power_one, mul_comm'] natCast := (fun n => lift.{u} #(Fin n) : ℕ → Cardinal.{u}) natCast_zero := rfl @@ -563,7 +563,7 @@ theorem power_bit1 (a b : Cardinal) : (a ^ bit1 b) = (a ^ b) * (a ^ b) * a := by end deprecated @[simp] -theorem one_power {a : Cardinal} : (1 ^ a) = 1 := +theorem one_power {a : Cardinal} : (1 ^ a : Cardinal) = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.one_power Cardinal.one_power @@ -578,7 +578,7 @@ theorem mk_Prop : #Prop = 2 := by simp #align cardinal.mk_Prop Cardinal.mk_Prop @[simp] -theorem zero_power {a : Cardinal} : a ≠ 0 → (0 ^ a) = 0 := +theorem zero_power {a : Cardinal} : a ≠ 0 → (0 ^ a : Cardinal) = 0 := inductionOn a fun _ heq => mk_eq_zero_iff.2 <| isEmpty_pi.2 <| @@ -586,7 +586,7 @@ theorem zero_power {a : Cardinal} : a ≠ 0 → (0 ^ a) = 0 := ⟨a, inferInstance⟩ #align cardinal.zero_power Cardinal.zero_power -theorem power_ne_zero {a : Cardinal} (b) : a ≠ 0 → (a ^ b) ≠ 0 := +theorem power_ne_zero {a : Cardinal} (b : Cardinal) : a ≠ 0 → (a ^ b) ≠ 0 := inductionOn₂ a b fun _ _ h => let ⟨a⟩ := mk_ne_zero_iff.1 h mk_ne_zero_iff.2 ⟨fun _ => a⟩ @@ -1346,7 +1346,7 @@ theorem card_le_of_finset {α} (s : Finset α) : (s.card : Cardinal) ≤ #α := -- Porting note: was `simp`. LHS is not normal form. -- @[simp, norm_cast] @[norm_cast] -theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = (m^n) := by +theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = (m : Cardinal) ^ (n : Cardinal) := by induction n <;> simp [pow_succ', power_add, *, Pow.pow] #align cardinal.nat_cast_pow Cardinal.natCast_pow @@ -2407,14 +2407,14 @@ theorem three_le {α : Type*} (h : 3 ≤ #α) (x : α) (y : α) : ∃ z : α, z /-- The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`. -/ def powerlt (a b : Cardinal.{u}) : Cardinal.{u} := - ⨆ c : Iio b, a^c + ⨆ c : Iio b, a ^ (c : Cardinal) #align cardinal.powerlt Cardinal.powerlt @[inherit_doc] infixl:80 " ^< " => powerlt theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : (a^c) ≤ a ^< b := by - refine le_ciSup (f := fun y : Iio b => a^y) ?_ ⟨c, h⟩ + refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩ rw [← image_eq_range] exact bddAbove_image.{u, u} _ bddAbove_Iio #align cardinal.le_powerlt Cardinal.le_powerlt diff --git a/Mathlib/SetTheory/Cardinal/Divisibility.lean b/Mathlib/SetTheory/Cardinal/Divisibility.lean index 0cb127333ca0f..aa01cfde5faab 100644 --- a/Mathlib/SetTheory/Cardinal/Divisibility.lean +++ b/Mathlib/SetTheory/Cardinal/Divisibility.lean @@ -150,7 +150,8 @@ theorem isPrimePow_iff {a : Cardinal} : IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n ⟨_, fun ⟨n, han, p, k, hp, hk, h⟩ => ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact_mod_cast h⟩⟩ rintro ⟨p, k, hp, hk, hpk⟩ - have key : p ^ 1 ≤ ↑a := by rw [←hpk]; apply power_le_power_left hp.ne_zero; exact_mod_cast hk + have key : p ^ (1 : Cardinal) ≤ ↑a := by + rw [←hpk]; apply power_le_power_left hp.ne_zero; exact_mod_cast hk rw [power_one] at key lift p to ℕ using key.trans_lt (nat_lt_aleph0 a) exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩ diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index d43ce11b7e73a..afbce477717f6 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -42,12 +42,12 @@ theorem zero_opow' (a : Ordinal) : (0^a) = 1 - a := by simp only [opow_def, if_t #align ordinal.zero_opow' Ordinal.zero_opow' @[simp] -theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0^a) = 0 := by +theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0 : Ordinal) ^ a = 0 := by rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero] #align ordinal.zero_opow Ordinal.zero_opow @[simp] -theorem opow_zero (a : Ordinal) : (a^0) = 1 := by +theorem opow_zero (a : Ordinal) : a ^ (0 : Ordinal) = 1 := by by_cases h : a = 0 · simp only [opow_def, if_pos h, sub_zero] · simp only [opow_def, if_neg h, limitRecOn_zero] @@ -74,12 +74,12 @@ theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) : #align ordinal.lt_opow_of_limit Ordinal.lt_opow_of_limit @[simp] -theorem opow_one (a : Ordinal) : (a^1) = a := by +theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a := by rw [← succ_zero, opow_succ]; simp only [opow_zero, one_mul] #align ordinal.opow_one Ordinal.opow_one @[simp] -theorem one_opow (a : Ordinal) : (1^a) = 1 := by +theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by induction a using limitRecOn with | H₁ => simp only [opow_zero] | H₂ _ ih => @@ -90,8 +90,8 @@ theorem one_opow (a : Ordinal) : (1^a) = 1 := by exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩ #align ordinal.one_opow Ordinal.one_opow -theorem opow_pos {a : Ordinal} (b) (a0 : 0 < a) : 0 < (a^b) := by - have h0 : 0 < (a^0) := by simp only [opow_zero, zero_lt_one] +theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by + have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one] induction b using limitRecOn with | H₁ => exact h0 | H₂ b IH => @@ -101,7 +101,7 @@ theorem opow_pos {a : Ordinal} (b) (a0 : 0 < a) : 0 < (a^b) := by exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩ #align ordinal.opow_pos Ordinal.opow_pos -theorem opow_ne_zero {a : Ordinal} (b) (a0 : a ≠ 0) : (a^b) ≠ 0 := +theorem opow_ne_zero {a : Ordinal} (b : Ordinal) (a0 : a ≠ 0) : a ^ b ≠ 0 := Ordinal.pos_iff_ne_zero.1 <| opow_pos b <| Ordinal.pos_iff_ne_zero.2 a0 #align ordinal.opow_ne_zero Ordinal.opow_ne_zero @@ -143,7 +143,7 @@ theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : ( simp only [one_opow, le_refl] #align ordinal.opow_le_opow_right Ordinal.opow_le_opow_right -theorem opow_le_opow_left {a b : Ordinal} (c) (ab : a ≤ b) : (a^c) ≤ (b^c) := by +theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c ≤ b ^ c := by by_cases a0 : a = 0 -- Porting note: `le_refl` is required. · subst a @@ -210,7 +210,7 @@ theorem opow_add (a b c : Ordinal) : a^(b + c) = (a^b) * (a^c) := by theorem opow_one_add (a b : Ordinal) : a^(1 + b) = a * (a^b) := by rw [opow_add, opow_one] #align ordinal.opow_one_add Ordinal.opow_one_add -theorem opow_dvd_opow (a) {b c : Ordinal} (h : b ≤ c) : (a^b) ∣ (a^c) := +theorem opow_dvd_opow (a : Ordinal) {b c : Ordinal} (h : b ≤ c) : (a^b) ∣ (a^c) := ⟨a^(c - b), by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]⟩ #align ordinal.opow_dvd_opow Ordinal.opow_dvd_opow @@ -258,7 +258,7 @@ def log (b : Ordinal) (x : Ordinal) : Ordinal := #align ordinal.log Ordinal.log /-- The set in the definition of `log` is nonempty. -/ -theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o | x < (b^o) }.Nonempty := +theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o : Ordinal | x < (b^o) }.Nonempty := ⟨_, succ_le_iff.1 (right_le_opow _ h)⟩ #align ordinal.log_nonempty Ordinal.log_nonempty @@ -296,8 +296,8 @@ theorem log_one_left : ∀ b, log 1 b = 0 := #align ordinal.log_one_left Ordinal.log_one_left theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : - succ (log b x) = sInf { o | x < (b^o) } := by - let t := sInf { o | x < (b^o) } + succ (log b x) = sInf { o : Ordinal | x < b ^ o } := by + let t := sInf { o : Ordinal | x < b ^ o } have : x < (b^t) := csInf_mem (log_nonempty hb) rcases zero_or_succ_or_limit t with (h | h | h) · refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim @@ -393,7 +393,8 @@ theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) exact opow_pos _ (zero_lt_one.trans hb) #align ordinal.log_mod_opow_log_lt_log_self Ordinal.log_mod_opow_log_lt_log_self -theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u) (hv : v ≠ 0) (w) : 0 < (b^u) * v + w := +theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u : Ordinal) (hv : v ≠ 0) (w : Ordinal) : + 0 < (b^u) * v + w := (opow_pos u <| Ordinal.pos_iff_ne_zero.2 hb).trans_le <| (le_mul_left _ <| Ordinal.pos_iff_ne_zero.2 hv).trans <| le_add_right _ _ #align ordinal.opow_mul_add_pos Ordinal.opow_mul_add_pos @@ -451,19 +452,19 @@ theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y /-! ### Interaction with `Nat.cast` -/ @[simp, norm_cast] -theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((m ^ n : ℕ) : Ordinal) = (m^n) +theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal) | 0 => by simp | n + 1 => by rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ] #align ordinal.nat_cast_opow Ordinal.nat_cast_opow -theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o^n) = (o^ω) := by +theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ (n : Ordinal)) = o ^ ω := by rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl) · exact (opow_isNormal ho₁).apply_omega · rw [one_opow] refine' le_antisymm (sup_le fun n => by rw [one_opow]) _ - convert le_sup (fun n : ℕ => 1^n) 0 - rw [Nat.cast_zero, opow_zero] + convert le_sup (fun n : ℕ => (1 : Ordinal) ^ n) 0 + rw [one_opow, one_pow] #align ordinal.sup_opow_nat Ordinal.sup_opow_nat end Ordinal diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index a1600f206cc20..6de1fb79e4e8b 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -889,9 +889,9 @@ set_option linter.unusedVariables false in theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω ∣ repr a') (e0 : repr a0 ≠ 0) (h : repr a' + m < (ω ^ repr a0)) (n : ℕ+) (k : ℕ) : let R := repr (opowAux 0 a0 (oadd a0 n a' * ofNat m) k m) - (k ≠ 0 → R < ((ω ^ repr a0) ^ succ ↑k)) ∧ - ((ω ^ repr a0) ^ k) * ((ω ^ repr a0) * (n : ℕ) + repr a') + R = - ((ω ^ repr a0) * (n : ℕ) + repr a' + m) ^ succ ↑k := by + (k ≠ 0 → R < ((ω ^ repr a0) ^ succ (k : Ordinal))) ∧ + ((ω ^ repr a0) ^ (k : Ordinal)) * ((ω ^ repr a0) * (n : ℕ) + repr a') + R = + ((ω ^ repr a0) * (n : ℕ) + repr a' + m) ^ succ (k : Ordinal) := by intro R' haveI No : NF (oadd a0 n a') := N0.oadd n (Na'.below_of_lt' <| lt_of_le_of_lt (le_add_right _ _) h) @@ -901,15 +901,16 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω let R := repr (opowAux 0 a0 (oadd a0 n a' * ofNat m) k m) let ω0 := ω ^ repr a0 let α' := ω0 * n + repr a' - change (k ≠ 0 → R < (ω0 ^ succ ↑k)) ∧ (ω0 ^ k) * α' + R = (α' + m) ^ succ ↑k at IH - have RR : R' = (ω0 ^ k) * (α' * m) + R := by + change (k ≠ 0 → R < (ω0 ^ succ (k : Ordinal))) ∧ (ω0 ^ (k : Ordinal)) * α' + R + = (α' + m) ^ (succ ↑k : Ordinal) at IH + have RR : R' = ω0 ^ (k : Ordinal) * (α' * m) + R := by by_cases h : m = 0 · simp only [h, ONote.ofNat, Nat.cast_zero, zero_add, ONote.repr, mul_zero, ONote.opowAux, add_zero] · simp only [ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux, ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add] have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a' - have ω00 : 0 < (ω0 ^ k) := opow_pos _ (opow_pos _ omega_pos) + have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega_pos) have Rl : R < ω ^ (repr a0 * succ ↑k) := by by_cases k0 : k = 0 · simp [k0] @@ -934,21 +935,22 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω (opow_le_opow_right omega_pos <| mul_le_mul_left' (succ_le_succ_iff.2 (nat_cast_le.2 (le_of_lt k.lt_succ_self))) _) calc - (ω0 ^ k.succ) * α' + R' - _ = (ω0 ^ succ ↑k) * α' + ((ω0 ^ k) * α' * m + R) := by rw [nat_cast_succ, RR, ← mul_assoc] - _ = ((ω0 ^ k) * α' + R) * α' + ((ω0 ^ k) * α' + R) * m := ?_ - _ = (α' + m) ^ succ ↑k.succ := by rw [← mul_add, nat_cast_succ, opow_succ, IH.2] + (ω0 ^ (k.succ : Ordinal)) * α' + R' + _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := + by rw [nat_cast_succ, RR, ← mul_assoc] + _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_ + _ = (α' + m) ^ succ (k.succ : Ordinal) := by rw [← mul_add, nat_cast_succ, opow_succ, IH.2] congr 1 · have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d - rw [mul_add (ω0^k), add_assoc, ← mul_assoc, ← opow_succ, + rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ, add_mul_limit _ (isLimit_iff_omega_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc, @mul_omega_dvd n (nat_cast_pos.2 n.pos) (nat_lt_omega _) _ αd] apply @add_absorp _ (repr a0 * succ ↑k) · refine' principal_add_omega_opow _ _ Rl rw [opow_mul, opow_succ, Ordinal.mul_lt_mul_iff_left ω00] exact No.snd'.repr_lt - · have := mul_le_mul_left' (one_le_iff_pos.2 <| nat_cast_pos.2 n.pos) (ω0^succ k) + · have := mul_le_mul_left' (one_le_iff_pos.2 <| nat_cast_pos.2 n.pos) (ω0 ^ succ (k : Ordinal)) rw [opow_mul] simpa [-opow_succ] · cases m diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean index 818dcae351052..53af177bf8aa8 100644 --- a/Mathlib/SetTheory/Ordinal/Principal.lean +++ b/Mathlib/SetTheory/Ordinal/Principal.lean @@ -202,7 +202,7 @@ theorem principal_add_omega_opow (o : Ordinal) : Principal (· + ·) (omega^o) : /-- The main characterization theorem for additive principal ordinals. -/ theorem principal_add_iff_zero_or_omega_opow {o : Ordinal} : - Principal (· + ·) o ↔ o = 0 ∨ ∃ a, o = (omega^a) := by + Principal (· + ·) o ↔ o = 0 ∨ ∃ a : Ordinal, o = (omega^a) := by rcases eq_or_ne o 0 with (rfl | ho) · simp only [principal_zero, Or.inl] · rw [principal_add_iff_add_left_eq_self] @@ -371,7 +371,7 @@ theorem principal_add_of_principal_mul_opow {o b : Ordinal} (hb : 1 < b) /-- The main characterization theorem for multiplicative principal ordinals. -/ theorem principal_mul_iff_le_two_or_omega_opow_opow {o : Ordinal} : - Principal (· * ·) o ↔ o ≤ 2 ∨ ∃ a, o = (omega^omega^a) := by + Principal (· * ·) o ↔ o ≤ 2 ∨ ∃ a : Ordinal, o = (omega^omega^a) := by refine' ⟨fun ho => _, _⟩ · cases' le_or_lt o 2 with ho₂ ho₂ · exact Or.inl ho₂ diff --git a/Mathlib/Topology/Algebra/Module/Cardinality.lean b/Mathlib/Topology/Algebra/Module/Cardinality.lean index 86dce76fac8dc..d87a1032f5c94 100644 --- a/Mathlib/Topology/Algebra/Module/Cardinality.lean +++ b/Mathlib/Topology/Algebra/Module/Cardinality.lean @@ -81,9 +81,9 @@ lemma cardinal_eq_of_mem_nhds_zero rw [zero_smul] at this filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s) exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn - have B : ∀ n, #(c^n • s) = #s := by + have B : ∀ n, #(c^n • s :) = #s := by intro n - have : c^n • s ≃ s := + have : (c^n • s :) ≃ s := { toFun := fun x ↦ ⟨(c^n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩ invFun := fun x ↦ ⟨(c^n) • x.1, smul_mem_smul_set x.2⟩ left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel (cn_ne n)] diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean b/Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean index f1139d116aa17..9a23271b177f5 100644 --- a/Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean +++ b/Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean @@ -66,7 +66,7 @@ theorem adic_basis (I : Ideal R) : SubmodulesRingBasis fun n : ℕ => (I ^ n • rintro a ⟨x, hx, rfl⟩ exact (I ^ n).smul_mem r hx mul := by - suffices ∀ i : ℕ, ∃ j : ℕ, (I ^ j: Set R) * (I ^ j : Set R) ⊆ (I ^ i : Set R) by + suffices ∀ i : ℕ, ∃ j : ℕ, (↑(I ^ j) * ↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R) by simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this intro n use n @@ -140,7 +140,7 @@ def openAddSubgroup (n : ℕ) : @OpenAddSubgroup R _ I.adicTopology := by letI := I.adicTopology refine ⟨(I ^ n).toAddSubgroup, ?_⟩ convert (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen - change (I ^ n : Set R) = (I ^ n • (⊤ : Ideal R) : Set R) + change (↑(I ^ n) : Set R) = ↑(I ^ n • (⊤ : Ideal R)) simp [smul_top_eq_map, Algebra.id.map_eq_id, map_id, restrictScalars_self] #align ideal.open_add_subgroup Ideal.openAddSubgroup diff --git a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean index 91d1e78667cb4..21728e0565122 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean @@ -519,7 +519,7 @@ theorem dimH_ball_pi (x : ι → ℝ) {r : ℝ} (hr : 0 < r) : exact fun x _ y _ => Subsingleton.elim x y · rw [← ENNReal.coe_nat] have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by - rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr, rpow_nat_cast] + rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr] refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_nat_cast, this] · simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)] · exact ENNReal.ofReal_ne_top diff --git a/test/positivity.lean b/test/positivity.lean index 631a878ae8c1c..ef3686a7c4917 100644 --- a/test/positivity.lean +++ b/test/positivity.lean @@ -182,7 +182,7 @@ example [LinearOrderedSemifield α] (a : α) : 0 < a ^ (0 : ℤ) := by positivit example {a b : ℝ} (ha : 0 ≤ a) : 0 ≤ a ^ b := by positivity example {a b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity -example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity +example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < (a : ℝ) ^ b := by positivity -- example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a ^ b := by positivity -- example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b := by positivity example {a : ℝ} : 0 < a ^ 0 := by positivity From 7569392b7099d22083f97f99cdaa691048c2ba28 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 8 Nov 2023 21:39:43 -0800 Subject: [PATCH 05/10] fixes --- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean | 2 +- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index 373f7578978e4..4caf7a61e230f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -268,7 +268,7 @@ lemma cpow_ofReal (x : ℂ) (y : ℝ) : lemma cpow_ofReal_re (x : ℂ) (y : ℝ) : (x ^ (y : ℂ)).re = (abs x) ^ y * Real.cos (arg x * y) := by rw [cpow_ofReal]; generalize arg x * y = z; simp [Real.cos] -lemma cpow_ofReal_im (x : ℂ) (y : ℝ) : (x ^ y).im = (abs x) ^ y * Real.sin (arg x * y) := by +lemma cpow_ofReal_im (x : ℂ) (y : ℝ) : (x ^ (y : ℂ)).im = (abs x) ^ y * Real.sin (arg x * y) := by rw [cpow_ofReal]; generalize arg x * y = z; simp [Real.sin] theorem abs_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) : diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index e56f6c784262a..9facc73f8ca09 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -79,7 +79,7 @@ theorem oangle_zero_right (x : V) : o.oangle x 0 = 0 := by simp [oangle] /-- If the two vectors passed to `oangle` are the same, the result is 0. -/ @[simp] theorem oangle_self (x : V) : o.oangle x x = 0 := by - rw [oangle, kahler_apply_self]; norm_cast + rw [oangle, kahler_apply_self, ← ofReal_pow]; norm_cast convert QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π)) apply arg_ofReal_of_nonneg positivity From c45a7756306580059b73856610cb3ea6fefb9ebf Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 9 Nov 2023 10:23:14 +0000 Subject: [PATCH 06/10] chore(SetTheory/Cardinal/Basic): make types more explicit When reading this file, it is difficult to tell whether statements are about ordinal or natural powers; especially given that when leanprover/lean4#2220 is fixed the meanings may change. This adds type annotations to remove the ambiguity. --- Mathlib/SetTheory/Cardinal/Basic.lean | 18 +++++++++--------- Mathlib/SetTheory/Ordinal/Exponential.lean | 20 ++++++++++---------- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index d0c7a4f1ab647..63b914bc2b0f0 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -508,12 +508,12 @@ theorem lift_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{ #align cardinal.lift_power Cardinal.lift_power @[simp] -theorem power_zero {a : Cardinal} : a ^ 0 = 1 := +theorem power_zero {a : Cardinal} : a ^ (0 : Cardinal) = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.power_zero Cardinal.power_zero @[simp] -theorem power_one {a : Cardinal.{u}} : a ^ 1 = a := +theorem power_one {a : Cardinal.{u}} : a ^ (1 : Cardinal) = a := inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α) #align cardinal.power_one Cardinal.power_one @@ -538,9 +538,9 @@ instance commSemiring : CommSemiring Cardinal.{u} where mul_comm := mul_comm' left_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.prodSumDistrib α β γ right_distrib a b c := inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumProdDistrib α β γ - npow n c := c ^ n + npow n c := c ^ (n : Cardinal) npow_zero := @power_zero - npow_succ n c := show c ^ (n + 1 : ℕ) = c * (c ^ n) + npow_succ n c := show c ^ (↑(n + 1) : Cardinal) = c * c ^ (↑n : Cardinal) by rw [Cardinal.cast_succ, power_add, power_one, mul_comm'] natCast := (fun n => lift.{u} #(Fin n) : ℕ → Cardinal.{u}) natCast_zero := rfl @@ -563,7 +563,7 @@ theorem power_bit1 (a b : Cardinal) : a ^ bit1 b = a ^ b * a ^ b * a := by end deprecated @[simp] -theorem one_power {a : Cardinal} : 1 ^ a = 1 := +theorem one_power {a : Cardinal} : (1 : Cardinal) ^ a = 1 := inductionOn a fun _ => mk_eq_one _ #align cardinal.one_power Cardinal.one_power @@ -578,7 +578,7 @@ theorem mk_Prop : #Prop = 2 := by simp #align cardinal.mk_Prop Cardinal.mk_Prop @[simp] -theorem zero_power {a : Cardinal} : a ≠ 0 → 0 ^ a = 0 := +theorem zero_power {a : Cardinal} : a ≠ 0 → (0 : Cardinal) ^ a = 0 := inductionOn a fun _ heq => mk_eq_zero_iff.2 <| isEmpty_pi.2 <| @@ -1347,7 +1347,7 @@ theorem card_le_of_finset {α} (s : Finset α) : (s.card : Cardinal) ≤ #α := -- Porting note: was `simp`. LHS is not normal form. -- @[simp, norm_cast] @[norm_cast] -theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = m ^ n := by +theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = (↑m : Cardinal) ^ (↑n : Cardinal) := by induction n <;> simp [pow_succ', power_add, *, Pow.pow] #align cardinal.nat_cast_pow Cardinal.natCast_pow @@ -2408,14 +2408,14 @@ theorem three_le {α : Type*} (h : 3 ≤ #α) (x : α) (y : α) : ∃ z : α, z /-- The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`. -/ def powerlt (a b : Cardinal.{u}) : Cardinal.{u} := - ⨆ c : Iio b, a^c + ⨆ c : Iio b, a ^ (c : Cardinal) #align cardinal.powerlt Cardinal.powerlt @[inherit_doc] infixl:80 " ^< " => powerlt theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : a ^ c ≤ a ^< b := by - refine le_ciSup (f := fun y : Iio b => a ^ y) ?_ ⟨c, h⟩ + refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩ rw [← image_eq_range] exact bddAbove_image.{u, u} _ bddAbove_Iio #align cardinal.le_powerlt Cardinal.le_powerlt diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index c8e20f4ca2d0c..5b66a07bd3479 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -42,12 +42,12 @@ theorem zero_opow' (a : Ordinal) : 0 ^ a = 1 - a := by simp only [opow_def, if_t #align ordinal.zero_opow' Ordinal.zero_opow' @[simp] -theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : 0 ^ a = 0 := by +theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0 : Ordinal) ^ a = 0 := by rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero] #align ordinal.zero_opow Ordinal.zero_opow @[simp] -theorem opow_zero (a : Ordinal) : a ^ 0 = 1 := by +theorem opow_zero (a : Ordinal) : a ^ (0 : Ordinal) = 1 := by by_cases h : a = 0 · simp only [opow_def, if_pos h, sub_zero] · simp only [opow_def, if_neg h, limitRecOn_zero] @@ -74,12 +74,12 @@ theorem lt_opow_of_limit {a b c : Ordinal} (b0 : b ≠ 0) (h : IsLimit c) : #align ordinal.lt_opow_of_limit Ordinal.lt_opow_of_limit @[simp] -theorem opow_one (a : Ordinal) : a ^ 1 = a := by +theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a := by rw [← succ_zero, opow_succ]; simp only [opow_zero, one_mul] #align ordinal.opow_one Ordinal.opow_one @[simp] -theorem one_opow (a : Ordinal) : 1 ^ a = 1 := by +theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by induction a using limitRecOn with | H₁ => simp only [opow_zero] | H₂ _ ih => @@ -91,7 +91,7 @@ theorem one_opow (a : Ordinal) : 1 ^ a = 1 := by #align ordinal.one_opow Ordinal.one_opow theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by - have h0 : 0 < a ^ 0 := by simp only [opow_zero, zero_lt_one] + have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one] induction b using limitRecOn with | H₁ => exact h0 | H₂ b IH => @@ -258,7 +258,7 @@ def log (b : Ordinal) (x : Ordinal) : Ordinal := #align ordinal.log Ordinal.log /-- The set in the definition of `log` is nonempty. -/ -theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o | x < b ^ o }.Nonempty := +theorem log_nonempty {b x : Ordinal} (h : 1 < b) : { o : Ordinal | x < b ^ o }.Nonempty := ⟨_, succ_le_iff.1 (right_le_opow _ h)⟩ #align ordinal.log_nonempty Ordinal.log_nonempty @@ -297,7 +297,7 @@ theorem log_one_left : ∀ b, log 1 b = 0 := theorem succ_log_def {b x : Ordinal} (hb : 1 < b) (hx : x ≠ 0) : succ (log b x) = sInf { o | x < b ^ o } := by - let t := sInf { o | x < b ^ o } + let t : Ordinal := sInf { o | x < b ^ o } have : x < b ^ t := csInf_mem (log_nonempty hb) rcases zero_or_succ_or_limit t with (h | h | h) · refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim @@ -452,18 +452,18 @@ theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y /-! ### Interaction with `Nat.cast` -/ @[simp, norm_cast] -theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((m ^ n : ℕ) : Ordinal) = m ^ n +theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal) | 0 => by simp | n + 1 => by rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ] #align ordinal.nat_cast_opow Ordinal.nat_cast_opow -theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ n) = o ^ ω := by +theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ (n : Ordinal)) = o ^ ω := by rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl) · exact (opow_isNormal ho₁).apply_omega · rw [one_opow] refine' le_antisymm (sup_le fun n => by rw [one_opow]) _ - convert le_sup (fun n : ℕ => 1 ^ n) 0 + convert le_sup (fun n : ℕ => 1 ^ (n : Ordinal)) 0 rw [Nat.cast_zero, opow_zero] #align ordinal.sup_opow_nat Ordinal.sup_opow_nat From ca50860c1a84a314ace36618ac0a94b8616ad4d9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 9 Nov 2023 10:27:50 +0000 Subject: [PATCH 07/10] revert regression --- Mathlib/SetTheory/Cardinal/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 63b914bc2b0f0..cc0d37a4d1111 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -2408,14 +2408,14 @@ theorem three_le {α : Type*} (h : 3 ≤ #α) (x : α) (y : α) : ∃ z : α, z /-- The function `a ^< b`, defined as the supremum of `a ^ c` for `c < b`. -/ def powerlt (a b : Cardinal.{u}) : Cardinal.{u} := - ⨆ c : Iio b, a ^ (c : Cardinal) + ⨆ c : Iio b, a ^ c #align cardinal.powerlt Cardinal.powerlt @[inherit_doc] infixl:80 " ^< " => powerlt theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : a ^ c ≤ a ^< b := by - refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩ + refine le_ciSup (f := fun y : Iio b => a ^ y) ?_ ⟨c, h⟩ rw [← image_eq_range] exact bddAbove_image.{u, u} _ bddAbove_Iio #align cardinal.le_powerlt Cardinal.le_powerlt From 149aa8b8a5162ab94a09160a676398856b3cd927 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 9 Nov 2023 15:45:13 -0800 Subject: [PATCH 08/10] fix --- Mathlib/Algebra/GradedMonoid.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean index 2342f2f95770e..463178b8a5ea6 100644 --- a/Mathlib/Algebra/GradedMonoid.lean +++ b/Mathlib/Algebra/GradedMonoid.lean @@ -321,7 +321,7 @@ section Monoid variable [AddMonoid ι] [GMonoid A] instance : NatPow (A 0) where - natPow x n := @Eq.rec ι (n • (0:ι)) (fun a _ => A a) (GMonoid.gnpow n x) 0 (nsmul_zero n) + pow x n := @Eq.rec ι (n • (0:ι)) (fun a _ => A a) (GMonoid.gnpow n x) 0 (nsmul_zero n) variable {A} From 6bb6ff23d68376d03a5df2370227102cd40f1a71 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 9 Nov 2023 16:14:59 -0800 Subject: [PATCH 09/10] review some fixes --- Mathlib/Algebra/CharZero/Quotient.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Stirling.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean index 8bcfbf76d972c..bf2cb7038ce32 100644 --- a/Mathlib/Algebra/CharZero/Quotient.lean +++ b/Mathlib/Algebra/CharZero/Quotient.lean @@ -53,7 +53,7 @@ end AddSubgroup namespace QuotientAddGroup theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) : - z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z : R) :) := by + z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R) := by induction ψ using Quotient.inductionOn' induction θ using Quotient.inductionOn' -- Porting note: Introduced Zp notation to shorten lines diff --git a/Mathlib/Analysis/SpecialFunctions/Stirling.lean b/Mathlib/Analysis/SpecialFunctions/Stirling.lean index 83fd055c26252..0f092d8efd5ab 100644 --- a/Mathlib/Analysis/SpecialFunctions/Stirling.lean +++ b/Mathlib/Analysis/SpecialFunctions/Stirling.lean @@ -75,7 +75,7 @@ theorem log_stirlingSeq_formula (n : ℕ) : `∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))` -/ theorem log_stirlingSeq_diff_hasSum (m : ℕ) : - HasSum (fun k : ℕ => ↑1 / (↑2 * ↑(k + 1) + ↑1) * (((1:ℝ)/(↑2 * (m + 1 :) + ↑1)) ^ 2) ^ ↑(k + 1)) + HasSum (fun k : ℕ => ↑1 / (↑2 * ↑(k + 1) + ↑1) * (((1:ℝ)/(↑2 * ↑(m + 1) + ↑1)) ^ 2) ^ ↑(k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))) := by change HasSum ((fun b : ℕ => (1:ℝ) / ((2:ℝ) * b + (1:ℝ)) * (((1:ℝ) / (2 * (m + 1 :) + 1)) ^ 2) ^ b) ∘ succ) _ From 5f16c539a4048e107d2e8f76816e95423850fb6d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sat, 11 Nov 2023 17:27:51 +1100 Subject: [PATCH 10/10] lint --- Mathlib/MeasureTheory/Covering/Differentiation.lean | 4 ++-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean | 2 +- Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/MeasureTheory/Covering/Differentiation.lean b/Mathlib/MeasureTheory/Covering/Differentiation.lean index 6757fff3105f4..009466fcc422f 100644 --- a/Mathlib/MeasureTheory/Covering/Differentiation.lean +++ b/Mathlib/MeasureTheory/Covering/Differentiation.lean @@ -572,7 +572,7 @@ theorem withDensity_le_mul {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico) simp only [M, withDensity_apply, coe_nnreal_smul_apply] calc - (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ x in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := + (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := lintegral_mono_ae ((ae_restrict_iff' M).2 (eventually_of_forall fun x hx => hx.2.2.le)) _ = (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter] @@ -642,7 +642,7 @@ theorem le_mul_withDensity {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht intro x hx apply hx.2.2.trans_le (le_of_eq _) rw [ENNReal.coe_zpow t_ne_zero'] - _ = ∫⁻ x in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by + _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter] _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by apply lintegral_mono_ae ((ae_restrict_iff' M).2 (eventually_of_forall fun x hx => ?_)) diff --git a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean index 2e82754471020..7ed4718d1723a 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean @@ -135,7 +135,7 @@ theorem integrable_comp_smul_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace (f : E → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun x => f (R • x)) μ ↔ Integrable f μ := by -- reduce to one-way implication suffices - ∀ {g : E → F} (hg : Integrable g μ) {S : ℝ} (hS : S ≠ 0), Integrable (fun x => g (S • x)) μ by + ∀ {g : E → F} (_ : Integrable g μ) {S : ℝ} (_ : S ≠ 0), Integrable (fun x => g (S • x)) μ by refine' ⟨fun hf => _, fun hf => this hf hR⟩ convert this hf (inv_ne_zero hR) rw [← mul_smul, mul_inv_cancel hR, one_smul] diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean index 9223c3f7ea701..406949c476890 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean @@ -343,10 +343,10 @@ def matrixToStdBasis : Matrix (index K) (index K) ℂ := theorem det_matrixToStdBasis : (matrixToStdBasis K).det = (2⁻¹ * I) ^ NrComplexPlaces K := calc - _ = ∏ k : { w : InfinitePlace K // IsComplex w }, det ((2 : ℂ)⁻¹ • !![1, 1; -I, I]) := by + _ = ∏ _k : { w : InfinitePlace K // IsComplex w }, det ((2 : ℂ)⁻¹ • !![1, 1; -I, I]) := by rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, Finset.prod_const_one, one_mul, det_reindex_self, det_blockDiagonal] - _ = ∏ k : { w : InfinitePlace K // IsComplex w }, (2⁻¹ * Complex.I) := by + _ = ∏ _k : { w : InfinitePlace K // IsComplex w }, (2⁻¹ * Complex.I) := by refine Finset.prod_congr (Eq.refl _) (fun _ _ => ?_) field_simp; ring _ = (2⁻¹ * Complex.I) ^ Fintype.card {w : InfinitePlace K // IsComplex w} := by