chore(Analysis/SpecialFunctions): Real.rpow -> _ ^ _ (#12613)

Mathlib/Analysis/SpecialFunctions/Log/Base.lean

@@ -160,7 +160,7 @@ theorem logb_eq_iff_rpow_eq (hy : 0 < y) : logb b y = x ↔ b ^ x = y := by
   · exact logb_rpow b_pos b_ne_one
 
 theorem surjOn_logb : SurjOn (logb b) (Ioi 0) univ := fun x _ =>
-  ⟨rpow b x, rpow_pos_of_pos b_pos x, logb_rpow b_pos b_ne_one⟩
+  ⟨b ^ x, rpow_pos_of_pos b_pos x, logb_rpow b_pos b_ne_one⟩
 #align real.surj_on_logb Real.surjOn_logb
 
 theorem logb_surjective : Surjective (logb b) := fun x => ⟨b ^ x, logb_rpow b_pos b_ne_one⟩

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -54,8 +54,7 @@ theorem tendsto_rpow_neg_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ =>
 
 open Asymptotics in
 lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b < 1) :
-    Tendsto (rpow b) atTop (𝓝 (0:ℝ)) := by
-  show Tendsto (fun z => b^z) atTop (𝓝 0)
+    Tendsto (b ^ · : ℝ → ℝ) atTop (𝓝 (0:ℝ)) := by
   rcases lt_trichotomy b 0 with hb|rfl|hb
   case inl => -- b < 0
     simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
@@ -80,21 +79,19 @@ lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b <
     exact (log_neg_iff hb).mpr hb₁
 
 lemma tendsto_rpow_atTop_of_base_gt_one (b : ℝ) (hb : 1 < b) :
-    Tendsto (rpow b) atBot (𝓝 (0:ℝ)) := by
-  show Tendsto (fun z => b^z) atBot (𝓝 0)
+    Tendsto (b ^ · : ℝ → ℝ) atBot (𝓝 (0:ℝ)) := by
   simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
   refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id
   exact (log_pos_iff (by positivity)).mpr <| by aesop
 
 lemma tendsto_rpow_atBot_of_base_lt_one (b : ℝ) (hb₀ : 0 < b) (hb₁ : b < 1) :
-    Tendsto (rpow b) atBot atTop := by
-  show Tendsto (fun z => b^z) atBot atTop
+    Tendsto (b ^ · : ℝ → ℝ) atBot atTop := by
   simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
   refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_
   exact (log_neg_iff hb₀).mpr hb₁
 
-lemma tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) : Tendsto (rpow b) atBot (𝓝 0) := by
-  show Tendsto (fun z => b^z) atBot (𝓝 0)
+lemma tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) :
+    Tendsto (b ^ · : ℝ → ℝ) atBot (𝓝 0) := by
   simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
   refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_iff_pos <| tendsto_id (α := ℝ)).mpr ?_
   exact (log_pos_iff (by positivity)).mpr <| by aesop

Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

@@ -92,7 +92,7 @@ theorem continuousAt_cpow {p : ℂ × ℂ} (hp_fst : p.fst ∈ slitPlane) :
 #align continuous_at_cpow continuousAt_cpow
 
 theorem continuousAt_cpow_const {a b : ℂ} (ha : a ∈ slitPlane) :
-    ContinuousAt (fun x => cpow x b) a :=
+    ContinuousAt (· ^ b) a :=
   Tendsto.comp (@continuousAt_cpow (a, b) ha) (continuousAt_id.prod continuousAt_const)
 #align continuous_at_cpow_const continuousAt_cpow_const
 
@@ -167,21 +167,15 @@ section RpowLimits
 
 namespace Real
 
-theorem continuousAt_const_rpow {a b : ℝ} (h : a ≠ 0) : ContinuousAt (rpow a) b := by
-  have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
-    ext1 x
-    rw [rpow_eq_pow, rpow_def]
-  rw [this]
-  refine' Complex.continuous_re.continuousAt.comp _
-  refine' (continuousAt_const_cpow _).comp Complex.continuous_ofReal.continuousAt
+theorem continuousAt_const_rpow {a b : ℝ} (h : a ≠ 0) : ContinuousAt (a ^ ·) b := by
+  simp only [rpow_def]
+  refine Complex.continuous_re.continuousAt.comp ?_
+  refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt
   norm_cast
 #align real.continuous_at_const_rpow Real.continuousAt_const_rpow
 
-theorem continuousAt_const_rpow' {a b : ℝ} (h : b ≠ 0) : ContinuousAt (rpow a) b := by
-  have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
-    ext1 x
-    rw [rpow_eq_pow, rpow_def]
-  rw [this]
+theorem continuousAt_const_rpow' {a b : ℝ} (h : b ≠ 0) : ContinuousAt (a ^ ·) b := by
+  simp only [rpow_def]
   refine' Complex.continuous_re.continuousAt.comp _
   refine' (continuousAt_const_cpow' _).comp Complex.continuous_ofReal.continuousAt
   norm_cast

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -810,26 +810,24 @@ lemma log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : log n ≤ n
   log_le_rpow_div n.cast_nonneg hε
 
 lemma strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) :
-    StrictMono (rpow b) := by
-  show StrictMono (fun (x:ℝ) => b ^ x)
+    StrictMono (b ^ · : ℝ → ℝ) := by
   simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
   exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb
 
 lemma monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) :
-    Monotone (rpow b) := by
+    Monotone (b ^ · : ℝ → ℝ) := by
   rcases lt_or_eq_of_le hb with hb | rfl
   case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
   case inr => intro _ _ _; simp
 
 lemma strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) :
-    StrictAnti (rpow b) := by
-  show StrictAnti (fun (x:ℝ) => b ^ x)
+    StrictAnti (b ^ · : ℝ → ℝ) := by
   simp_rw [Real.rpow_def_of_pos hb₀]
   exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
       <| Real.log_neg hb₀ hb₁
 
 lemma antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) :
-    Antitone (rpow b) := by
+    Antitone (b ^ · : ℝ → ℝ) := by
   rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
   case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
   case inr => intro _ _ _; simp

Mathlib/Topology/MetricSpace/Holder.lean

@@ -119,16 +119,16 @@ theorem edist_le_of_le (h : HolderOnWith C r f s) {x y : X} (hx : x ∈ s) (hy :
 
 theorem comp {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0}
     {f : X → Y} (hf : HolderOnWith Cf rf f s) (hst : MapsTo f s t) :
-    HolderOnWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g ∘ f) s := by
+    HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s := by
   intro x hx y hy
-  rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc, NNReal.rpow_eq_pow,
+  rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc,
     ← ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]
   exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)
 #align holder_on_with.comp HolderOnWith.comp
 
 theorem comp_holderWith {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t)
     {Cf rf : ℝ≥0} {f : X → Y} (hf : HolderWith Cf rf f) (ht : ∀ x, f x ∈ t) :
-    HolderWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g ∘ f) :=
+    HolderWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
   holderOnWith_univ.mp <| hg.comp (hf.holderOnWith univ) fun x _ => ht x
 #align holder_on_with.comp_holder_with HolderOnWith.comp_holderWith
 
@@ -199,13 +199,13 @@ theorem edist_le_of_le (h : HolderWith C r f) {x y : X} {d : ℝ≥0∞} (hd : e
 #align holder_with.edist_le_of_le HolderWith.edist_le_of_le
 
 theorem comp {Cg rg : ℝ≥0} {g : Y → Z} (hg : HolderWith Cg rg g) {Cf rf : ℝ≥0} {f : X → Y}
-    (hf : HolderWith Cf rf f) : HolderWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g ∘ f) :=
+    (hf : HolderWith Cf rf f) : HolderWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
   (hg.holderOnWith univ).comp_holderWith hf fun _ => trivial
 #align holder_with.comp HolderWith.comp
 
 theorem comp_holderOnWith {Cg rg : ℝ≥0} {g : Y → Z} (hg : HolderWith Cg rg g) {Cf rf : ℝ≥0}
     {f : X → Y} {s : Set X} (hf : HolderOnWith Cf rf f s) :
-    HolderOnWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g ∘ f) s :=
+    HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s :=
   (hg.holderOnWith univ).comp hf fun _ _ => trivial
 #align holder_with.comp_holder_on_with HolderWith.comp_holderOnWith