bump to nightly-2023-07-02-17

mathlib commit leanprover-community/mathlib@9240e8b

Mathbin/Algebra/Order/Field/Basic.lean

@@ -1353,7 +1353,7 @@ theorem max_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : max (a / c) (b /
 -/
 
 #print abs_inv /-
-theorem abs_inv (a : α) : |a⁻¹| = (|a|)⁻¹ :=
+theorem abs_inv (a : α) : |a⁻¹| = |a|⁻¹ :=
   map_inv₀ (absHom : α →*₀ α) a
 #align abs_inv abs_inv
 -/

Mathbin/Algebra/Order/Group/Abs.lean

@@ -97,7 +97,7 @@ theorem abs_le_abs (h₀ : a ≤ b) (h₁ : -a ≤ b) : |a| ≤ |b| :=
 -/
 
 #print abs_by_cases /-
-theorem abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (|a|) :=
+theorem abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P |a| :=
   sup_ind _ _ h1 h2
 #align abs_by_cases abs_by_cases
 -/
@@ -335,7 +335,7 @@ theorem le_of_abs_le (h : |a| ≤ b) : a ≤ b :=
 @[to_additive]
 theorem apply_abs_le_mul_of_one_le' {β : Type _} [MulOneClass β] [Preorder β]
     [CovariantClass β β (· * ·) (· ≤ ·)] [CovariantClass β β (swap (· * ·)) (· ≤ ·)] {f : α → β}
-    {a : α} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f (|a|) ≤ f a * f (-a) :=
+    {a : α} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a) :=
   (le_total a 0).byCases (fun ha => (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁) fun ha =>
     (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂
 #align apply_abs_le_mul_of_one_le' apply_abs_le_mul_of_one_le'
@@ -346,7 +346,7 @@ theorem apply_abs_le_mul_of_one_le' {β : Type _} [MulOneClass β] [Preorder β]
 @[to_additive]
 theorem apply_abs_le_mul_of_one_le {β : Type _} [MulOneClass β] [Preorder β]
     [CovariantClass β β (· * ·) (· ≤ ·)] [CovariantClass β β (swap (· * ·)) (· ≤ ·)] {f : α → β}
-    (h : ∀ x, 1 ≤ f x) (a : α) : f (|a|) ≤ f a * f (-a) :=
+    (h : ∀ x, 1 ≤ f x) (a : α) : f |a| ≤ f a * f (-a) :=
   apply_abs_le_mul_of_one_le' (h _) (h _)
 #align apply_abs_le_mul_of_one_le apply_abs_le_mul_of_one_le
 #align apply_abs_le_add_of_nonneg apply_abs_le_add_of_nonneg
@@ -357,7 +357,7 @@ theorem apply_abs_le_mul_of_one_le {β : Type _} [MulOneClass β] [Preorder β]
 -/
 theorem abs_add (a b : α) : |a + b| ≤ |a| + |b| :=
   abs_le.2
-    ⟨(neg_add (|a|) (|b|)).symm ▸
+    ⟨(neg_add |a| |b|).symm ▸
         add_le_add (neg_le.2 <| neg_le_abs_self _) (neg_le.2 <| neg_le_abs_self _),
       add_le_add (le_abs_self _) (le_abs_self _)⟩
 #align abs_add abs_add
@@ -435,36 +435,36 @@ theorem abs_eq (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b :=
 -/
 
 #print abs_le_max_abs_abs /-
-theorem abs_le_max_abs_abs (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max (|a|) (|c|) :=
+theorem abs_le_max_abs_abs (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max |a| |c| :=
   abs_le'.2
     ⟨by simp [hbc.trans (le_abs_self c)], by
       simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs_self a)]⟩
 #align abs_le_max_abs_abs abs_le_max_abs_abs
 -/
 
 #print min_abs_abs_le_abs_max /-
-theorem min_abs_abs_le_abs_max : min (|a|) (|b|) ≤ |max a b| :=
+theorem min_abs_abs_le_abs_max : min |a| |b| ≤ |max a b| :=
   (le_total a b).elim (fun h => (min_le_right _ _).trans_eq <| congr_arg _ (max_eq_right h).symm)
     fun h => (min_le_left _ _).trans_eq <| congr_arg _ (max_eq_left h).symm
 #align min_abs_abs_le_abs_max min_abs_abs_le_abs_max
 -/
 
 #print min_abs_abs_le_abs_min /-
-theorem min_abs_abs_le_abs_min : min (|a|) (|b|) ≤ |min a b| :=
+theorem min_abs_abs_le_abs_min : min |a| |b| ≤ |min a b| :=
   (le_total a b).elim (fun h => (min_le_left _ _).trans_eq <| congr_arg _ (min_eq_left h).symm)
     fun h => (min_le_right _ _).trans_eq <| congr_arg _ (min_eq_right h).symm
 #align min_abs_abs_le_abs_min min_abs_abs_le_abs_min
 -/
 
 #print abs_max_le_max_abs_abs /-
-theorem abs_max_le_max_abs_abs : |max a b| ≤ max (|a|) (|b|) :=
+theorem abs_max_le_max_abs_abs : |max a b| ≤ max |a| |b| :=
   (le_total a b).elim (fun h => (congr_arg _ <| max_eq_right h).trans_le <| le_max_right _ _)
     fun h => (congr_arg _ <| max_eq_left h).trans_le <| le_max_left _ _
 #align abs_max_le_max_abs_abs abs_max_le_max_abs_abs
 -/
 
 #print abs_min_le_max_abs_abs /-
-theorem abs_min_le_max_abs_abs : |min a b| ≤ max (|a|) (|b|) :=
+theorem abs_min_le_max_abs_abs : |min a b| ≤ max |a| |b| :=
   (le_total a b).elim (fun h => (congr_arg _ <| min_eq_left h).trans_le <| le_max_left _ _) fun h =>
     (congr_arg _ <| min_eq_right h).trans_le <| le_max_right _ _
 #align abs_min_le_max_abs_abs abs_min_le_max_abs_abs

Mathbin/Algebra/Order/Group/MinMax.lean

@@ -108,7 +108,7 @@ theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b
 -/
 
 #print abs_max_sub_max_le_max /-
-theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max (|a - c|) (|b - d|) :=
+theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d| :=
   by
   refine' abs_sub_le_iff.2 ⟨_, _⟩
   · exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
@@ -118,7 +118,7 @@ theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max (|a
 -/
 
 #print abs_min_sub_min_le_max /-
-theorem abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max (|a - c|) (|b - d|) := by
+theorem abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max |a - c| |b - d| := by
   simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
     abs_max_sub_max_le_max (-a) (-b) (-c) (-d)
 #align abs_min_sub_min_le_max abs_min_sub_min_le_max

Mathbin/Algebra/Order/LatticeGroup.lean

@@ -415,7 +415,7 @@ theorem m_neg_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁻
 @[to_additive pos_abs]
 theorem m_pos_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a|⁺ = |a| :=
   by
-  nth_rw 2 [← pos_div_neg (|a|)]
+  nth_rw 2 [← pos_div_neg |a|]
   rw [div_eq_mul_inv]
   symm
   rw [mul_right_eq_self, inv_eq_one]

Mathbin/Algebra/Parity.lean

@@ -219,7 +219,7 @@ theorem Even.neg_one_zpow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow,
 end DivisionMonoid
 
 #print even_abs /-
-theorem even_abs [SubtractionMonoid α] [LinearOrder α] {a : α} : Even (|a|) ↔ Even a := by
+theorem even_abs [SubtractionMonoid α] [LinearOrder α] {a : α} : Even |a| ↔ Even a := by
   cases abs_choice a <;> simp only [h, even_neg]
 #align even_abs even_abs
 -/

Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -28,14 +28,18 @@ noncomputable instance : ChartedSpace ℂ ℍ :=
 instance : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
   UpperHalfPlane.openEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
 
+#print UpperHalfPlane.smooth_coe /-
 /-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
 theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := fun x => contMDiffAt_extChartAt
 #align upper_half_plane.smooth_coe UpperHalfPlane.smooth_coe
+-/
 
+#print UpperHalfPlane.mdifferentiable_coe /-
 /-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
-theorem mDifferentiable_coe : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
+theorem mdifferentiable_coe : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
   smooth_coe.MDifferentiable
-#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mDifferentiable_coe
+#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mdifferentiable_coe
+-/
 
 end UpperHalfPlane
 

Mathbin/Analysis/Convex/Gauge.lean

@@ -354,7 +354,7 @@ theorem gauge_smul_left_of_nonneg [MulActionWithZero α E] [SMulCommClass α ℝ
 #print gauge_smul_left /-
 theorem gauge_smul_left [Module α E] [SMulCommClass α ℝ ℝ] [IsScalarTower α ℝ ℝ]
     [IsScalarTower α ℝ E] {s : Set E} (symmetric : ∀ x ∈ s, -x ∈ s) (a : α) :
-    gauge (a • s) = (|a|)⁻¹ • gauge s :=
+    gauge (a • s) = |a|⁻¹ • gauge s :=
   by
   rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]
   obtain h | h := abs_choice a

Mathbin/Analysis/InnerProductSpace/Basic.lean

@@ -1939,7 +1939,7 @@ itself, divided by the product of their norms, has value 1. -/
 theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {x : F} {r : ℝ} (hx : x ≠ 0)
     (hr : 0 < r) : ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1 :=
   by
-  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ (|r|),
+  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
     mul_assoc, abs_of_nonneg hr.le, div_self]
   exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))
 #align real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul
@@ -1951,7 +1951,7 @@ itself, divided by the product of their norms, has value -1. -/
 theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {x : F} {r : ℝ} (hx : x ≠ 0)
     (hr : r < 0) : ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1 :=
   by
-  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ (|r|),
+  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
     mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]
   exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))
 #align real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul

Mathbin/Analysis/MellinTransform.lean

@@ -163,7 +163,7 @@ theorem mellin_div_const (f : ℝ → ℂ) (s a : ℂ) : mellin (fun t => f t /
 
 #print mellin_comp_rpow /-
 theorem mellin_comp_rpow (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : a ≠ 0) :
-    mellin (fun t => f (t ^ a)) s = (|a|)⁻¹ • mellin f (s / a) :=
+    mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / a) :=
   by
   -- note: this is also true for a = 0 (both sides are zero), but this is mathematically
   -- uninteresting and rather time-consuming to check

Mathbin/Analysis/Normed/Group/AddCircle.lean

@@ -64,8 +64,7 @@ theorem norm_coe_mul (x : ℝ) (t : ℝ) :
   congr 1
   ext z
   rw [mem_smul_set_iff_inv_smul_mem₀ ht']
-  show
-    (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ |w| = (|t|)⁻¹ * z
+  show (∃ y, y - t * x ∈ zmultiples (t * p) ∧ |y| = z) ↔ ∃ w, w - x ∈ zmultiples p ∧ |w| = |t|⁻¹ * z
   constructor
   · rintro ⟨y, hy, rfl⟩
     refine' ⟨t⁻¹ * y, _, by rw [abs_mul, abs_inv]⟩

Mathbin/Analysis/Normed/Group/Basic.lean

@@ -2105,7 +2105,7 @@ theorem ennnorm_eq_ofReal (hr : 0 ≤ r) : (‖r‖₊ : ℝ≥0∞) = ENNReal.o
 -/
 
 #print Real.ennnorm_eq_ofReal_abs /-
-theorem ennnorm_eq_ofReal_abs (r : ℝ) : (‖r‖₊ : ℝ≥0∞) = ENNReal.ofReal (|r|) := by
+theorem ennnorm_eq_ofReal_abs (r : ℝ) : (‖r‖₊ : ℝ≥0∞) = ENNReal.ofReal |r| := by
   rw [← Real.nnnorm_abs r, Real.ennnorm_eq_ofReal (abs_nonneg _)]
 #align real.ennnorm_eq_of_real_abs Real.ennnorm_eq_ofReal_abs
 -/

Mathbin/Analysis/SpecialFunctions/CompareExp.lean

@@ -157,14 +157,14 @@ This is the main lemma in the proof of `complex.is_exp_cmp_filter.is_o_cpow_exp`
 theorem isLittleO_log_abs_re (hl : IsExpCmpFilter l) : (fun z => Real.log (abs z)) =o[l] re :=
   calc
     (fun z => Real.log (abs z)) =O[l] fun z =>
-        Real.log (Real.sqrt 2) + Real.log (max z.re (|z.im|)) :=
+        Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|) :=
       IsBigO.of_bound 1 <|
         (hl.tendsto_re.eventually_ge_atTop 1).mono fun z hz =>
           by
           have h2 : 0 < Real.sqrt 2 := by simp
           have hz' : 1 ≤ abs z := hz.trans (re_le_abs z)
           have hz₀ : 0 < abs z := one_pos.trans_le hz'
-          have hm₀ : 0 < max z.re (|z.im|) := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
+          have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
           rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')]
           refine' le_trans _ (le_abs_self _)
           rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
@@ -176,7 +176,7 @@ theorem isLittleO_log_abs_re (hl : IsExpCmpFilter l) : (fun z => Real.log (abs z
           filter_upwards [is_o_iff_nat_mul_le.1 hl.is_o_log_re_re n,
             hl.abs_im_pow_eventually_le_exp_re n, hl.tendsto_re.eventually_gt_at_top 1] with z hre
             him h₁
-          cases' le_total (|z.im|) z.re with hle hle
+          cases' le_total |z.im| z.re with hle hle
           · rwa [max_eq_left hle]
           · have H : 1 < |z.im| := h₁.trans_le hle
             rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),

Mathbin/Analysis/SpecialFunctions/Log/Base.lean

@@ -69,7 +69,7 @@ theorem logb_one : logb b 1 = 0 := by simp [logb]
 
 #print Real.logb_abs /-
 @[simp]
-theorem logb_abs (x : ℝ) : logb b (|x|) = logb b x := by rw [logb, logb, log_abs]
+theorem logb_abs (x : ℝ) : logb b |x| = logb b x := by rw [logb, logb, log_abs]
 #align real.logb_abs Real.logb_abs
 -/
 

Mathbin/Analysis/SpecialFunctions/Log/Basic.lean

@@ -128,7 +128,7 @@ theorem log_one : log 1 = 0 :=
 
 #print Real.log_abs /-
 @[simp]
-theorem log_abs (x : ℝ) : log (|x|) = log x :=
+theorem log_abs (x : ℝ) : log |x| = log x :=
   by
   by_cases h : x = 0
   · simp [h]

Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean

@@ -314,7 +314,7 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
       sub_ne_zero_of_ne (ne_of_lt hy.2)]
     ring
   -- second step: show that the derivative of `F` is small
-  have B : ∀ y ∈ Icc (-|x|) (|x|), |deriv F y| ≤ |x| ^ n / (1 - |x|) :=
+  have B : ∀ y ∈ Icc (-|x|) |x|, |deriv F y| ≤ |x| ^ n / (1 - |x|) :=
     by
     intro y hy
     have : y ∈ Ioo (-(1 : ℝ)) 1 := ⟨lt_of_lt_of_le (neg_lt_neg h) hy.1, lt_of_le_of_lt hy.2 h⟩
@@ -329,7 +329,7 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
   -- third step: apply the mean value inequality
   have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ :=
     by
-    have : ∀ y ∈ Icc (-|x|) (|x|), DifferentiableAt ℝ F y :=
+    have : ∀ y ∈ Icc (-|x|) |x|, DifferentiableAt ℝ F y :=
       by
       intro y hy
       have : 1 - y ≠ 0 := sub_ne_zero_of_ne (ne_of_gt (lt_of_le_of_lt hy.2 h))

Mathbin/Analysis/SpecialFunctions/Pow/Continuity.lean

@@ -415,7 +415,7 @@ theorem continuousAt_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) :
         (continuous_fst.norm.tendsto _).rpow ((continuous_re.comp continuous_snd).Tendsto _) _ <;>
       simp [hz, Real.zero_rpow hz.ne']
   · simp only [(· ∘ ·), Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
-    rcases exists_gt (|im z|) with ⟨C, hC⟩
+    rcases exists_gt |im z| with ⟨C, hC⟩
     refine' ⟨Real.exp (π * C), eventually_map.2 _⟩
     refine'
       (((continuous_im.comp continuous_snd).abs.Tendsto (_, z)).Eventually (gt_mem_nhds hC)).mono

Mathbin/Analysis/SpecialFunctions/Trigonometric/Angle.lean

@@ -1262,13 +1262,13 @@ theorem sign_toReal {θ : Angle} (h : θ ≠ π) : SignType.sign θ.toReal = θ.
 -/
 
 #print Real.Angle.coe_abs_toReal_of_sign_nonneg /-
-theorem coe_abs_toReal_of_sign_nonneg {θ : Angle} (h : 0 ≤ θ.sign) : ↑(|θ.toReal|) = θ := by
+theorem coe_abs_toReal_of_sign_nonneg {θ : Angle} (h : 0 ≤ θ.sign) : ↑|θ.toReal| = θ := by
   rw [abs_eq_self.2 (to_real_nonneg_iff_sign_nonneg.2 h), coe_to_real]
 #align real.angle.coe_abs_to_real_of_sign_nonneg Real.Angle.coe_abs_toReal_of_sign_nonneg
 -/
 
 #print Real.Angle.neg_coe_abs_toReal_of_sign_nonpos /-
-theorem neg_coe_abs_toReal_of_sign_nonpos {θ : Angle} (h : θ.sign ≤ 0) : -↑(|θ.toReal|) = θ :=
+theorem neg_coe_abs_toReal_of_sign_nonpos {θ : Angle} (h : θ.sign ≤ 0) : -↑|θ.toReal| = θ :=
   by
   rw [SignType.nonpos_iff] at h 
   rcases h with (h | h)

Mathbin/Analysis/SpecialFunctions/Trigonometric/Basic.lean

@@ -1871,11 +1871,11 @@ $$\left|exp^{a\left(e^{z}+e^{-z}\right)}\right| \le e^{a\cos b \exp^{|re z|}}.$$
 -/
 theorem abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le {a b : ℝ} (ha : a ≤ 0) {z : ℂ} (hz : |z.im| ≤ b)
     (hb : b ≤ π / 2) :
-    abs (exp (a * (exp z + exp (-z)))) ≤ Real.exp (a * Real.cos b * Real.exp (|z.re|)) :=
+    abs (exp (a * (exp z + exp (-z)))) ≤ Real.exp (a * Real.cos b * Real.exp |z.re|) :=
   by
   simp only [abs_exp, Real.exp_le_exp, of_real_mul_re, add_re, exp_re, neg_im, Real.cos_neg, ←
     add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
-  have : Real.exp (|z.re|) ≤ Real.exp z.re + Real.exp (-z.re) :=
+  have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
     apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
   refine' mul_le_mul_of_nonpos_left (mul_le_mul this _ _ ((Real.exp_pos _).le.trans this)) ha
   ·

Mathbin/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -991,7 +991,7 @@ theorem sinh_nonneg_iff : 0 ≤ sinh x ↔ 0 ≤ x := by simpa only [sinh_zero]
 -/
 
 #print Real.abs_sinh /-
-theorem abs_sinh (x : ℝ) : |sinh x| = sinh (|x|) := by
+theorem abs_sinh (x : ℝ) : |sinh x| = sinh |x| := by
   cases le_total x 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]
 #align real.abs_sinh Real.abs_sinh
 -/

Mathbin/Analysis/SpecificLimits/Normed.lean

@@ -275,7 +275,7 @@ theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr :
     exact
       tendsto_const_nhds.congr'
         (mem_at_top_sets.2 ⟨1, fun n hn => by simp [zero_lt_one.trans_le hn, h0]⟩)
-  have hr' : 1 < (|r|)⁻¹ := one_lt_inv (abs_pos.2 h0) hr
+  have hr' : 1 < |r|⁻¹ := one_lt_inv (abs_pos.2 h0) hr
   rw [tendsto_zero_iff_norm_tendsto_zero]
   simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'
 #align tendsto_pow_const_mul_const_pow_of_abs_lt_one tendsto_pow_const_mul_const_pow_of_abs_lt_one

Mathbin/Data/Complex/Basic.lean

@@ -1269,7 +1269,7 @@ theorem abs_le_abs_re_add_abs_im (z : ℂ) : abs z ≤ |z.re| + |z.im| := by
 -/
 
 #print Complex.abs_le_sqrt_two_mul_max /-
-theorem abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ Real.sqrt 2 * max (|z.re|) (|z.im|) :=
+theorem abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ Real.sqrt 2 * max |z.re| |z.im| :=
   by
   cases' z with x y
   simp only [abs_apply, norm_sq_mk, ← sq]
@@ -1278,7 +1278,7 @@ theorem abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ Real.sqrt 2 * max (|z.re|)
   calc
     Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt (y ^ 2 + y ^ 2) :=
       Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
-    _ = Real.sqrt 2 * max (|x|) (|y|) := by
+    _ = Real.sqrt 2 * max |x| |y| := by
       rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
 #align complex.abs_le_sqrt_two_mul_max Complex.abs_le_sqrt_two_mul_max
 -/
@@ -1306,8 +1306,7 @@ theorem abs_cast_nat (n : ℕ) : abs (n : ℂ) = n := by
 
 #print Complex.int_cast_abs /-
 @[simp, norm_cast]
-theorem int_cast_abs (n : ℤ) : ↑(|n|) = abs n := by
-  rw [← of_real_int_cast, abs_of_real, Int.cast_abs]
+theorem int_cast_abs (n : ℤ) : ↑|n| = abs n := by rw [← of_real_int_cast, abs_of_real, Int.cast_abs]
 #align complex.int_cast_abs Complex.int_cast_abs
 -/
 

Mathbin/Data/Complex/Exponential.lean

@@ -1508,7 +1508,7 @@ theorem cos_neg : cos (-x) = cos x := by simp [cos, exp_neg]
 
 #print Real.cos_abs /-
 @[simp]
-theorem cos_abs : cos (|x|) = cos x := by
+theorem cos_abs : cos |x| = cos x := by
   cases le_total x 0 <;> simp only [*, _root_.abs_of_nonneg, abs_of_nonpos, cos_neg]
 #align real.cos_abs Real.cos_abs
 -/
@@ -1784,7 +1784,7 @@ theorem cosh_neg : cosh (-x) = cosh x :=
 
 #print Real.cosh_abs /-
 @[simp]
-theorem cosh_abs : cosh (|x|) = cosh x := by
+theorem cosh_abs : cosh |x| = cosh x := by
   cases le_total x 0 <;> simp [*, _root_.abs_of_nonneg, abs_of_nonpos]
 #align real.cosh_abs Real.cosh_abs
 -/

Mathbin/Data/Int/Order/Basic.lean

@@ -78,13 +78,13 @@ theorem coe_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| :=
 -/
 
 #print Nat.cast_natAbs /-
-theorem Nat.cast_natAbs {α : Type _} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = ↑(|n|) := by
+theorem Nat.cast_natAbs {α : Type _} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = ↑|n| := by
   rw [← Int.coe_natAbs, Int.cast_ofNat]
 #align nat.cast_nat_abs Nat.cast_natAbs
 -/
 
 #print Int.natAbs_abs /-
-theorem natAbs_abs (a : ℤ) : natAbs (|a|) = natAbs a := by rw [abs_eq_nat_abs] <;> rfl
+theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a := by rw [abs_eq_nat_abs] <;> rfl
 #align int.nat_abs_abs Int.natAbs_abs
 -/
 

Mathbin/Data/Real/Ereal.lean

@@ -1395,7 +1395,7 @@ a real `x` to `|x|`. -/
 protected def abs : EReal → ℝ≥0∞
   | ⊥ => ⊤
   | ⊤ => ⊤
-  | (x : ℝ) => ENNReal.ofReal (|x|)
+  | (x : ℝ) => ENNReal.ofReal |x|
 #align ereal.abs EReal.abs
 -/
 
@@ -1414,7 +1414,7 @@ theorem abs_bot : (⊥ : EReal).abs = ⊤ :=
 -/
 
 #print EReal.abs_def /-
-theorem abs_def (x : ℝ) : (x : EReal).abs = ENNReal.ofReal (|x|) :=
+theorem abs_def (x : ℝ) : (x : EReal).abs = ENNReal.ofReal |x| :=
   rfl
 #align ereal.abs_def EReal.abs_def
 -/