leanprover-community · kim-em · Nov 9, 2023 · Oct 28, 2023 · Oct 28, 2023 · Oct 29, 2023
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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/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/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
@@ -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
@@ -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/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
@@ -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
@@ -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
@@ -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/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean
@@ -320,7 +320,7 @@ section Monoid
 
 variable [AddMonoid ι] [GMonoid A]
 
-instance : Pow (A 0) ℕ where
+instance : NatPow (A 0) where
   pow 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/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/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/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
@@ -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
@@ -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
@@ -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/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/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/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand Down @@