chore(analysis/normed/field/basic): add @[simp] to `real.norm_eq_abs (

#15006)

* mark `real.norm_eq_abs` and `abs_nonneg` as `simp` lemmas;
* add `abs` versions of `is_o.norm_left` etc;
* add `inner_product_geometry.angle_smul_smul` and `linear_isometry.angle_map`.

archive/imo/imo1972_q5.lean

@@ -43,7 +43,7 @@ begin
   have hk₂ : ∀ x, 2 * (∥f x∥ * ∥g y∥) ≤ 2 * k,
   { intro x,
     calc 2 * (∥f x∥ * ∥g y∥)
-        = ∥2 * f x * g y∥ : by simp [real.norm_eq_abs, abs_mul, mul_assoc]
+        = ∥2 * f x * g y∥ : by simp [abs_mul, mul_assoc]
     ... = ∥f (x + y) + f (x - y)∥ : by rw hf1
     ... ≤ ∥f (x + y)∥ + ∥f (x - y)∥ : norm_add_le _ _
     ... ≤ k + k : add_le_add (hk₁ _) (hk₁ _)

counterexamples/seminorm_lattice_not_distrib.lean

@@ -36,10 +36,9 @@ by { use 0, rintro _ ⟨x, rfl⟩, exact add_nonneg (p.nonneg _) (q.nonneg _) }
 
 lemma eq_one : (p ⊔ (q1 ⊓ q2)) (1, 1) = 1 :=
 begin
-  dsimp [p, -seminorm.inf_apply],
-  rw [sup_idem, norm_one, sup_eq_left],
+  suffices : (⨅ x : ℝ × ℝ, q1 x + q2 (1 - x)) ≤ 1, by simpa,
   apply cinfi_le_of_le (bdd_below_range_add _ _ _) ((0, 1) : ℝ×ℝ), dsimp [q1, q2],
-  simp only [norm_zero, smul_zero, sub_self, add_zero, zero_le_one],
+  simp only [abs_zero, smul_zero, sub_self, add_zero, zero_le_one],
 end
 
 /-- This is a counterexample to the distributivity of the lattice `seminorm ℝ (ℝ × ℝ)`. -/

src/algebra/order/group.lean

@@ -1080,7 +1080,7 @@ end
 lemma neg_abs_le_neg (a : α) : -|a| ≤ -a :=
 by simpa using neg_abs_le_self (-a)
 
-lemma abs_nonneg (a : α) : 0 ≤ |a| :=
+@[simp] lemma abs_nonneg (a : α) : 0 ≤ |a| :=
 (le_total 0 a).elim (λ h, h.trans (le_abs_self a)) (λ h, (neg_nonneg.2 h).trans $ neg_le_abs_self a)
 
 @[simp] lemma abs_abs (a : α) : | |a| | = |a| :=

src/analysis/asymptotics/asymptotics.lean

@@ -420,52 +420,94 @@ is_o.of_is_O_with $ λ c cpos, (h.forall_is_O_with cpos).sup (h'.forall_is_O_wit
 @[simp] lemma is_o_sup : f =o[l ⊔ l'] g ↔ f =o[l] g ∧ f =o[l'] g :=
 ⟨λ h, ⟨h.mono le_sup_left, h.mono le_sup_right⟩, λ h, h.1.sup h.2⟩
 
-/-! ### Simplification : norm -/
+/-! ### Simplification : norm, abs -/
+
+section norm_abs
+
+variables {u v : α → ℝ}
 
 @[simp] theorem is_O_with_norm_right : is_O_with c l f (λ x, ∥g' x∥) ↔ is_O_with c l f g' :=
 by simp only [is_O_with, norm_norm]
 
+@[simp] theorem is_O_with_abs_right : is_O_with c l f (λ x, |u x|) ↔ is_O_with c l f u :=
+@is_O_with_norm_right _ _ _ _ _ _ f u l
+
 alias is_O_with_norm_right ↔ is_O_with.of_norm_right is_O_with.norm_right
+alias is_O_with_abs_right ↔ is_O_with.of_abs_right is_O_with.abs_right
 
 @[simp] theorem is_O_norm_right : f =O[l] (λ x, ∥g' x∥) ↔ f =O[l] g' :=
 by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_right) }
 
+@[simp] theorem is_O_abs_right : f =O[l] (λ x, |u x|) ↔ f =O[l] u :=
+@is_O_norm_right _ _ ℝ _ _ _ _ _
+
 alias is_O_norm_right ↔ is_O.of_norm_right is_O.norm_right
+alias is_O_abs_right ↔ is_O.of_abs_right is_O.abs_right
 
 @[simp] theorem is_o_norm_right : f =o[l] (λ x, ∥g' x∥) ↔ f =o[l] g' :=
 by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_right) }
 
+@[simp] theorem is_o_abs_right : f =o[l] (λ x, |u x|) ↔ f =o[l] u :=
+@is_o_norm_right _ _ ℝ _ _ _ _ _
+
 alias is_o_norm_right ↔ is_o.of_norm_right is_o.norm_right
+alias is_o_abs_right ↔ is_o.of_abs_right is_o.abs_right
 
 @[simp] theorem is_O_with_norm_left : is_O_with c l (λ x, ∥f' x∥) g ↔ is_O_with c l f' g :=
 by simp only [is_O_with, norm_norm]
 
+@[simp] theorem is_O_with_abs_left : is_O_with c l (λ x, |u x|) g ↔ is_O_with c l u g :=
+@is_O_with_norm_left _ _ _ _ _ _ g u l
+
 alias is_O_with_norm_left ↔ is_O_with.of_norm_left is_O_with.norm_left
+alias is_O_with_abs_left ↔ is_O_with.of_abs_left is_O_with.abs_left
 
 @[simp] theorem is_O_norm_left : (λ x, ∥f' x∥) =O[l] g ↔ f' =O[l] g :=
 by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_left) }
 
+@[simp] theorem is_O_abs_left : (λ x, |u x|) =O[l] g ↔ u =O[l] g :=
+@is_O_norm_left _ _ _ _ _ g u l
+
 alias is_O_norm_left ↔ is_O.of_norm_left is_O.norm_left
+alias is_O_abs_left ↔ is_O.of_abs_left is_O.abs_left
 
 @[simp] theorem is_o_norm_left : (λ x, ∥f' x∥) =o[l] g ↔ f' =o[l] g :=
 by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_left) }
 
+@[simp] theorem is_o_abs_left : (λ x, |u x|) =o[l] g ↔ u =o[l] g :=
+@is_o_norm_left _ _ _ _ _ g u l
+
 alias is_o_norm_left ↔ is_o.of_norm_left is_o.norm_left
+alias is_o_abs_left ↔ is_o.of_abs_left is_o.abs_left
 
 theorem is_O_with_norm_norm : is_O_with c l (λ x, ∥f' x∥) (λ x, ∥g' x∥) ↔ is_O_with c l f' g' :=
 is_O_with_norm_left.trans is_O_with_norm_right
 
+theorem is_O_with_abs_abs : is_O_with c l (λ x, |u x|) (λ x, |v x|) ↔ is_O_with c l u v :=
+is_O_with_abs_left.trans is_O_with_abs_right
+
 alias is_O_with_norm_norm ↔ is_O_with.of_norm_norm is_O_with.norm_norm
+alias is_O_with_abs_abs ↔ is_O_with.of_abs_abs is_O_with.abs_abs
 
 theorem is_O_norm_norm : (λ x, ∥f' x∥) =O[l] (λ x, ∥g' x∥) ↔ f' =O[l] g' :=
 is_O_norm_left.trans is_O_norm_right
 
+theorem is_O_abs_abs : (λ x, |u x|) =O[l] (λ x, |v x|) ↔ u =O[l] v :=
+is_O_abs_left.trans is_O_abs_right
+
 alias is_O_norm_norm ↔ is_O.of_norm_norm is_O.norm_norm
+alias is_O_abs_abs ↔ is_O.of_abs_abs is_O.abs_abs
 
 theorem is_o_norm_norm : (λ x, ∥f' x∥) =o[l] (λ x, ∥g' x∥) ↔ f' =o[l] g' :=
 is_o_norm_left.trans is_o_norm_right
 
+theorem is_o_abs_abs : (λ x, |u x|) =o[l] (λ x, |v x|) ↔ u =o[l] v :=
+is_o_abs_left.trans is_o_abs_right
+
 alias is_o_norm_norm ↔ is_o.of_norm_norm is_o.norm_norm
+alias is_o_abs_abs ↔ is_o.of_abs_abs is_o.abs_abs
+
+end norm_abs
 
 /-! ### Simplification: negate -/
 
@@ -615,7 +657,7 @@ is_o.of_is_O_with $ λ c cpos, ((h₁.forall_is_O_with $ half_pos cpos).add
 theorem is_o.add_add (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
   (λ x, f₁ x + f₂ x) =o[l] (λ x, ∥g₁ x∥ + ∥g₂ x∥) :=
 by refine (h₁.trans_le $ λ x, _).add (h₂.trans_le _);
-  simp [real.norm_eq_abs, abs_of_nonneg, add_nonneg]
+  simp [abs_of_nonneg, add_nonneg]
 
 theorem is_O.add_is_o (h₁ : f₁ =O[l] g) (h₂ : f₂ =o[l] g) : (λ x, f₁ x + f₂ x) =O[l] g :=
 h₁.add h₂.is_O

src/analysis/calculus/fderiv.lean

@@ -2857,7 +2857,7 @@ begin
   symmetry,
   rw [tendsto_iff_norm_tendsto_zero], refine tendsto_congr (λ x', _),
   have : ∥x' - x∥⁻¹ ≥ 0, from inv_nonneg.mpr (norm_nonneg _),
-  simp [norm_smul, real.norm_eq_abs, abs_of_nonneg this]
+  simp [norm_smul, abs_of_nonneg this]
 end
 
 lemma has_fderiv_at.lim_real (hf : has_fderiv_at f f' x) (v : E) :

src/analysis/complex/basic.lean

@@ -161,7 +161,7 @@ by simpa [mul_self_abs] using
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def re_clm : ℂ →L[ℝ] ℝ := re_lm.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_re_le_abs])
+def re_clm : ℂ →L[ℝ] ℝ := re_lm.mk_continuous 1 (λ x, by simp [abs_re_le_abs])
 
 @[continuity] lemma continuous_re : continuous re := re_clm.continuous
 
@@ -177,7 +177,7 @@ calc 1 = ∥re_clm 1∥ : by simp
 @[simp] lemma re_clm_nnnorm : ∥re_clm∥₊ = 1 := subtype.ext re_clm_norm
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def im_clm : ℂ →L[ℝ] ℝ := im_lm.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_im_le_abs])
+def im_clm : ℂ →L[ℝ] ℝ := im_lm.mk_continuous 1 (λ x, by simp [abs_im_le_abs])
 
 @[continuity] lemma continuous_im : continuous im := im_clm.continuous
 

src/analysis/normed/group/basic.lean

@@ -111,7 +111,7 @@ noncomputable instance : normed_group ℝ :=
 { norm := λ x, |x|,
   dist_eq := assume x y, rfl }
 
-lemma real.norm_eq_abs (r : ℝ) : ∥r∥ = |r| := rfl
+@[simp] lemma real.norm_eq_abs (r : ℝ) : ∥r∥ = |r| := rfl
 
 section semi_normed_group
 variables [semi_normed_group E] [semi_normed_group F] [semi_normed_group G]

src/analysis/normed_space/basic.lean

@@ -173,12 +173,12 @@ def homeomorph_unit_ball {E : Type*} [semi_normed_group E] [normed_space ℝ E]
   left_inv := λ x,
     begin
       have : 0 < 1 + ∥x∥ := (norm_nonneg x).trans_lt (lt_one_add _),
-      field_simp [this.ne', abs_of_pos this, norm_smul, smul_smul, real.norm_eq_abs, abs_div]
+      field_simp [this.ne', abs_of_pos this, norm_smul, smul_smul, abs_div]
     end,
   right_inv := λ x, subtype.ext
     begin
       have : 0 < 1 - ∥(x : E)∥ := sub_pos.2 (mem_ball_zero_iff.1 x.2),
-      field_simp [norm_smul, smul_smul, real.norm_eq_abs, abs_div, abs_of_pos this, this.ne']
+      field_simp [norm_smul, smul_smul, abs_div, abs_of_pos this, this.ne']
     end,
   continuous_to_fun := continuous_subtype_mk _ $
     ((continuous_const.add continuous_norm).inv₀

src/analysis/special_functions/log/deriv.lean

@@ -230,7 +230,7 @@ begin
       have : 1 - y ≠ 0 := sub_ne_zero_of_ne (ne_of_gt (lt_of_le_of_lt hy.2 h)),
       simp [F, this] },
     apply convex.norm_image_sub_le_of_norm_deriv_le this B (convex_Icc _ _) _ _,
-    { simpa using abs_nonneg x },
+    { simp },
     { simp [le_abs_self x, neg_le.mp (neg_le_abs_self x)] } },
   -- fourth step: conclude by massaging the inequality of the third step
   simpa [F, norm_eq_abs, div_mul_eq_mul_div, pow_succ'] using C

src/geometry/euclidean/basic.lean

@@ -80,22 +80,24 @@ real.continuous_arccos.continuous_at.comp $ continuous_inner.continuous_at.div
   ((continuous_norm.comp continuous_fst).mul (continuous_norm.comp continuous_snd)).continuous_at
   (by simp [hx1, hx2])
 
+lemma angle_smul_smul {c : ℝ} (hc : c ≠ 0) (x y : V) :
+  angle (c • x) (c • y) = angle x y :=
+have c * c ≠ 0, from mul_ne_zero hc hc,
+by rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, real.norm_eq_abs,
+  mul_mul_mul_comm _ (∥x∥), abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
+
+@[simp] lemma _root_.linear_isometry.angle_map {E F : Type*}
+  [inner_product_space ℝ E] [inner_product_space ℝ F] (f : E →ₗᵢ[ℝ] F) (u v : E) :
+  angle (f u) (f v) = angle u v :=
+by rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
+
 lemma is_conformal_map.preserves_angle {E F : Type*}
   [inner_product_space ℝ E] [inner_product_space ℝ F]
   {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
   angle (f' u) (f' v) = angle u v :=
 begin
-  obtain ⟨c, hc, li, hcf⟩ := h,
-  suffices : c * (c * inner u v) / (∥c∥ * ∥u∥ * (∥c∥ * ∥v∥)) = inner u v / (∥u∥ * ∥v∥),
-  { simp [this, angle, hcf, norm_smul, inner_smul_left, inner_smul_right] },
-  by_cases hu : ∥u∥ = 0,
-  { simp [norm_eq_zero.mp hu] },
-  by_cases hv : ∥v∥ = 0,
-  { simp [norm_eq_zero.mp hv] },
-  have hc : ∥c∥ ≠ 0 := λ w, hc (norm_eq_zero.mp w),
-  field_simp,
-  have : c * c = ∥c∥ * ∥c∥ := by simp [real.norm_eq_abs, abs_mul_abs_self],
-  convert congr_arg (λ x, x * ⟪u, v⟫ * ∥u∥ * ∥v∥) this using 1; ring,
+  obtain ⟨c, hc, li, rfl⟩ := h,
+  exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)
 end
 
 /-- If a real differentiable map `f` is conformal at a point `x`,

src/geometry/euclidean/inversion.lean

@@ -58,7 +58,7 @@ lemma dist_inversion_center (c x : P) (R : ℝ) : dist (inversion c R x) c = R ^
 begin
   rcases eq_or_ne x c with (rfl|hx), { simp },
   have : dist x c ≠ 0, from dist_ne_zero.2 hx,
-  field_simp [inversion, norm_smul, norm_eq_abs, abs_div, ← dist_eq_norm_vsub, sq, mul_assoc]
+  field_simp [inversion, norm_smul, abs_div, ← dist_eq_norm_vsub, sq, mul_assoc]
 end
 
 /-- Distance from the center of an inversion to the image of a point under the inversion. This

src/geometry/euclidean/sphere.lean

@@ -77,9 +77,9 @@ begin
       = ∥(r - 1) • y∥ * ∥(r + 1) • y∥      : by simp [sub_smul, add_smul, hxy]
   ... = ∥r - 1∥ * ∥y∥ * (∥r + 1∥ * ∥y∥)      : by simp_rw [norm_smul]
   ... = ∥r - 1∥ * ∥r + 1∥ * ∥y∥ ^ 2         : by ring
-  ... = |(r - 1) * (r + 1) * ∥y∥ ^ 2| : by simp [abs_mul, norm_eq_abs]
+  ... = |(r - 1) * (r + 1) * ∥y∥ ^ 2| : by simp [abs_mul]
   ... = |r ^ 2 * ∥y∥ ^ 2 - ∥y∥ ^ 2|    : by ring_nf
-  ... = |∥x∥ ^ 2 - ∥y∥ ^ 2|            : by simp [hxy, norm_smul, mul_pow, norm_eq_abs, sq_abs]
+  ... = |∥x∥ ^ 2 - ∥y∥ ^ 2|            : by simp [hxy, norm_smul, mul_pow, sq_abs]
   ... = |∥z + y∥ ^ 2 - ∥z - x∥ ^ 2|    : by simp [norm_add_sq_real, norm_sub_sq_real,
                                                     hzy, hzx, abs_sub_comm],
 end

src/geometry/manifold/instances/sphere.lean

@@ -187,7 +187,7 @@ begin
   { have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp [inner_smul_left, hvy],
     convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2,
     { simp [← split] },
-    { simp [norm_smul, hv, real.norm_eq_abs, ← sq, sq_abs] },
+    { simp [norm_smul, hv, ← sq, sq_abs] },
     { exact sq _ } },
   -- two facts which will be helpful for clearing denominators in the main calculation
   have ha : 1 - a ≠ 0,

src/measure_theory/function/l1_space.lean

@@ -344,12 +344,12 @@ section pos_part
 
 lemma has_finite_integral.max_zero {f : α → ℝ} (hf : has_finite_integral f μ) :
   has_finite_integral (λa, max (f a) 0) μ :=
-hf.mono $ eventually_of_forall $ λ x, by simp [real.norm_eq_abs, abs_le, abs_nonneg, le_abs_self]
+hf.mono $ eventually_of_forall $ λ x, by simp [abs_le, le_abs_self]
 
 lemma has_finite_integral.min_zero {f : α → ℝ} (hf : has_finite_integral f μ) :
   has_finite_integral (λa, min (f a) 0) μ :=
 hf.mono $ eventually_of_forall $ λ x,
-  by simp [real.norm_eq_abs, abs_le, abs_nonneg, neg_le, neg_le_abs_self, abs_eq_max_neg, le_total]
+  by simp [abs_le, neg_le, neg_le_abs_self, abs_eq_max_neg, le_total]
 
 end pos_part
 
@@ -687,7 +687,7 @@ begin
   refine lt_of_le_of_lt _ ((has_finite_integral_iff_norm _).1 hf.has_finite_integral),
   apply lintegral_mono,
   assume x,
-  simp [real.norm_eq_abs, ennreal.of_real_le_of_real, abs_le, abs_nonneg, le_abs_self],
+  simp [ennreal.of_real_le_of_real, abs_le, le_abs_self],
 end
 
 lemma of_real_to_real_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) :

src/measure_theory/function/l2_space.lean

@@ -33,7 +33,7 @@ variables {α F : Type*} {m : measurable_space α} {μ : measure α} [normed_gro
 
 lemma mem_ℒp.integrable_sq {f : α → ℝ} (h : mem_ℒp f 2 μ) :
   integrable (λ x, (f x)^2) μ :=
-by simpa [real.norm_eq_abs, ← mem_ℒp_one_iff_integrable]
+by simpa [← mem_ℒp_one_iff_integrable]
   using h.norm_rpow ennreal.two_ne_zero ennreal.two_ne_top
 
 lemma mem_ℒp_two_iff_integrable_sq_norm {f : α → F} (hf : ae_strongly_measurable f μ) :
@@ -50,7 +50,7 @@ lemma mem_ℒp_two_iff_integrable_sq {f : α → ℝ} (hf : ae_strongly_measurab
 begin
   convert mem_ℒp_two_iff_integrable_sq_norm hf,
   ext x,
-  simp [real.norm_eq_abs],
+  simp,
 end
 
 end

src/measure_theory/integral/bochner.lean

@@ -1137,7 +1137,7 @@ begin
   by_cases hfm : ae_strongly_measurable f μ,
   { refine integral_mono_ae ⟨hfm, _⟩ hgi h,
     refine (hgi.has_finite_integral.mono $ h.mp $ hf.mono $ λ x hf hfg, _),
-    simpa [real.norm_eq_abs, abs_of_nonneg hf, abs_of_nonneg (le_trans hf hfg)] },
+    simpa [abs_of_nonneg hf, abs_of_nonneg (le_trans hf hfg)] },
   { rw [integral_non_ae_strongly_measurable hfm],
     exact integral_nonneg_of_ae (hf.trans h) }
 end

src/measure_theory/integral/circle_integral.lean

@@ -120,7 +120,7 @@ lemma circle_map_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ ball c R)
 @[simp] lemma range_circle_map (c : ℂ) (R : ℝ) : range (circle_map c R) = sphere c (|R|) :=
 calc range (circle_map c R) = c +ᵥ R • range (λ θ : ℝ, exp (θ * I)) :
   by simp only [← image_vadd, ← image_smul, ← range_comp, vadd_eq_add, circle_map, (∘), real_smul]
-... = sphere c (|R|) : by simp [smul_sphere R (0 : ℂ) zero_le_one, real.norm_eq_abs]
+... = sphere c (|R|) : by simp [smul_sphere R (0 : ℂ) zero_le_one]
 
 /-- The image of `(0, 2π]` under `circle_map c R` is the circle with center `c` and radius `|R|`. -/
 @[simp] lemma image_circle_map_Ioc (c : ℂ) (R : ℝ) :

src/measure_theory/measure/haar_lebesgue.lean

@@ -419,15 +419,15 @@ lemma add_haar_closed_ball_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ) :
   μ (closed_ball x (r * s)) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (closed_ball 0 s) :=
 begin
   have : closed_ball (0 : E) (r * s) = r • closed_ball 0 s,
-    by simp [smul_closed_ball' hr.ne' (0 : E), real.norm_eq_abs, abs_of_nonneg hr.le],
+    by simp [smul_closed_ball' hr.ne' (0 : E), abs_of_nonneg hr.le],
   simp only [this, add_haar_smul, abs_of_nonneg hr.le, add_haar_closed_ball_center, abs_pow],
 end
 
 lemma add_haar_closed_ball_mul (x : E) {r : ℝ} (hr : 0 ≤ r) {s : ℝ} (hs : 0 ≤ s) :
   μ (closed_ball x (r * s)) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (closed_ball 0 s) :=
 begin
   have : closed_ball (0 : E) (r * s) = r • closed_ball 0 s,
-    by simp [smul_closed_ball r (0 : E) hs, real.norm_eq_abs, abs_of_nonneg hr],
+    by simp [smul_closed_ball r (0 : E) hs, abs_of_nonneg hr],
   simp only [this, add_haar_smul, abs_of_nonneg hr, add_haar_closed_ball_center, abs_pow],
 end
 

src/number_theory/padics/hensel.lean

@@ -106,22 +106,19 @@ lt_of_le_of_ne (norm_nonneg _) (ne.symm deriv_norm_ne_zero)
 private lemma deriv_ne_zero : F.derivative.eval a ≠ 0 := mt norm_eq_zero.2 deriv_norm_ne_zero
 
 private lemma T_def : T = ∥F.eval a∥ / ∥F.derivative.eval a∥^2 :=
-calc T = ∥F.eval a∥ / ∥((F.derivative.eval a)^2 : ℚ_[p])∥ : norm_div _ _
-   ... = ∥F.eval a∥ / ∥(F.derivative.eval a)^2∥ : by simp [norm, padic_int.norm_def]
-   ... = ∥F.eval a∥ / ∥(F.derivative.eval a)∥^2 : by simp
+by simp [T, ← padic_int.norm_def]
 
 private lemma T_lt_one : T < 1 :=
 let h := (div_lt_one deriv_sq_norm_pos).2 hnorm in
 by rw T_def; apply h
 
-private lemma T_pow {n : ℕ} (hn : n > 0) : T ^ n < 1 :=
-have T ^ n ≤ T ^ 1,
-from pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) (succ_le_of_lt hn),
-lt_of_le_of_lt (by simpa) T_lt_one
+private lemma T_nonneg : 0 ≤ T := norm_nonneg _
 
-private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := (T_pow (pow_pos (by norm_num) _))
+private lemma T_pow_nonneg (n : ℕ) : 0 ≤ T ^ n := pow_nonneg T_nonneg _
 
-private lemma T_pow_nonneg (n : ℕ) : 0 ≤ T ^ n := pow_nonneg (norm_nonneg _) _
+private lemma T_pow {n : ℕ} (hn : n ≠ 0) : T ^ n < 1 := pow_lt_one T_nonneg T_lt_one hn
+
+private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := T_pow (pow_ne_zero _ two_ne_zero)
 
 /-- We will construct a sequence of elements of ℤ_p satisfying successive values of `ih`. -/
 private def ih (n : ℕ) (z : ℤ_[p]) : Prop :=
@@ -152,7 +149,7 @@ calc
   (div_le_div_right deriv_norm_pos).2 hz.2
 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel _ _
 ... < ∥F.derivative.eval a∥ :
-  (mul_lt_iff_lt_one_right deriv_norm_pos).2 (T_pow (pow_pos (by norm_num) _))
+  (mul_lt_iff_lt_one_right deriv_norm_pos).2 (T_pow' _)
 
 private def calc_eval_z'  {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n z)
   (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
@@ -319,15 +316,13 @@ begin
 end
 
 private lemma bound : ∀ {ε}, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → ∥F.derivative.eval a∥ * T^(2^n) < ε :=
-have mtn : ∀ n : ℕ, ∥polynomial.eval a (polynomial.derivative F)∥ * T ^ (2 ^ n) ≥ 0,
-  from λ n, mul_nonneg (norm_nonneg _) (T_pow_nonneg _),
 begin
   have := bound' hnorm hnsol,
   simp [tendsto, nhds] at this,
   intros ε hε,
   cases this (ball 0 ε) (mem_ball_self hε) (is_open_ball) with N hN,
   existsi N, intros n hn,
-  simpa [norm_mul, real.norm_eq_abs, abs_of_nonneg (mtn n)] using hN _ hn
+  simpa [abs_of_nonneg (T_nonneg _)] using hN _ hn
 end
 
 private lemma bound'_sq : tendsto (λ n : ℕ, ∥F.derivative.eval a∥^2 * T^(2^n)) at_top (𝓝 0) :=