chore(analysis/normed_space): add 2 @[simp] attrs (#4775)

Add `@[simp]` to `norm_pos_iff` and `norm_le_zero_iff`

src/analysis/normed_space/basic.lean

@@ -156,10 +156,10 @@ lemma norm_sum_le_of_le {β} (s : finset β) {f : β → α} {n : β → ℝ} (h
   ∥∑ b in s, f b∥ ≤ ∑ b in s, n b :=
 le_trans (norm_sum_le s f) (finset.sum_le_sum h)
 
-lemma norm_pos_iff {g : α} : 0 < ∥ g ∥ ↔ g ≠ 0 :=
+@[simp] lemma norm_pos_iff {g : α} : 0 < ∥ g ∥ ↔ g ≠ 0 :=
 dist_zero_right g ▸ dist_pos
 
-lemma norm_le_zero_iff {g : α} : ∥g∥ ≤ 0 ↔ g = 0 :=
+@[simp] lemma norm_le_zero_iff {g : α} : ∥g∥ ≤ 0 ↔ g = 0 :=
 by { rw[←dist_zero_right], exact dist_le_zero }
 
 lemma norm_sub_le (g h : α) : ∥g - h∥ ≤ ∥g∥ + ∥h∥ :=

src/analysis/normed_space/multilinear.lean

@@ -350,10 +350,9 @@ begin
   split,
   { assume h,
     ext m,
-    simpa [h, norm_le_zero_iff.symm] using f.le_op_norm m },
-  { assume h,
-    apply le_antisymm (op_norm_le_bound f (le_refl _) (λm, _)) (op_norm_nonneg _),
-    rw h,
+    simpa [h] using f.le_op_norm m },
+  { rintro rfl,
+    apply le_antisymm (op_norm_le_bound 0 le_rfl (λm, _)) (op_norm_nonneg _),
     simp }
 end
 

src/analysis/normed_space/units.lean

@@ -103,9 +103,7 @@ lemma inverse_add (x : units R) :
 begin
   nontriviality R,
   rw [eventually_iff, mem_nhds_iff],
-  have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹,
-  { cancel_denoms,
-    exact x⁻¹.norm_pos },
+  have hinv : 0 < ∥(↑x⁻¹ : R)∥⁻¹, by cancel_denoms,
   use [∥(↑x⁻¹ : R)∥⁻¹, hinv],
   intros t ht,
   simp only [mem_ball, dist_zero_right] at ht,
@@ -116,7 +114,7 @@ begin
     cancel_denoms },
   have hright := inverse_one_sub (-↑x⁻¹ * t) ht',
   have hleft := inverse_unit (x.add t ht),
-  simp only [neg_mul_eq_neg_mul_symm, sub_neg_eq_add] at hright,
+  simp only [← neg_mul_eq_neg_mul, sub_neg_eq_add] at hright,
   simp only [units.add_coe] at hleft,
   simp [hleft, hright, units.add]
 end

src/data/padics/hensel.lean

@@ -424,7 +424,7 @@ include hnorm
 private lemma a_is_soln (ha : F.eval a = 0) :
   F.eval a = 0 ∧ ∥a - a∥ < ∥F.derivative.eval a∥ ∧ ∥F.derivative.eval a∥ = ∥F.derivative.eval a∥ ∧
   ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = a :=
-⟨ha, by simp; apply deriv_norm_pos; apply hnorm, rfl, a_soln_is_unique ha⟩
+⟨ha, by simp [deriv_ne_zero hnorm], rfl, a_soln_is_unique ha⟩
 
 lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥ ∧
   ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧