chore(data/padics/*): linting + squeeze_simp speedup (#4531)

src/data/padics/padic_norm.lean

@@ -531,6 +531,13 @@ padic_norm_p_lt_one $ nat.prime.one_lt ‹_›
 protected theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padic_norm p q = p ^ (-z) :=
 ⟨ (padic_val_rat p q), by simp [padic_norm, hq] ⟩
 
+/--
+`padic_norm p` is symmetric.
+-/
+@[simp] protected lemma neg (q : ℚ) : padic_norm p (-q) = padic_norm p q :=
+if hq : q = 0 then by simp [hq]
+else by simp [padic_norm, hq]
+
 variable [hp : fact p.prime]
 include hp
 
@@ -544,13 +551,6 @@ begin
   exact_mod_cast ne_of_gt hp.pos
 end
 
-/--
-`padic_norm p` is symmetric.
--/
-@[simp] protected lemma neg (q : ℚ) : padic_norm p (-q) = padic_norm p q :=
-if hq : q = 0 then by simp [hq]
-else by simp [padic_norm, hq, hp.one_lt]
-
 /--
 If the p-adic norm of `q` is 0, then `q` is 0.
 -/

src/data/padics/padic_numbers.lean

@@ -62,7 +62,7 @@ open_locale classical
 open nat multiplicity padic_norm cau_seq cau_seq.completion metric
 
 /-- The type of Cauchy sequences of rationals with respect to the p-adic norm. -/
-@[reducible] def padic_seq (p : ℕ) [fact p.prime] := cau_seq _ (padic_norm p)
+@[reducible] def padic_seq (p : ℕ) := cau_seq _ (padic_norm p)
 
 namespace padic_seq
 
@@ -265,10 +265,10 @@ include hp
 lemma norm_mul (f g : padic_seq p) : (f * g).norm = f.norm * g.norm :=
 if hf : f ≈ 0 then
   have hg : f * g ≈ 0, from mul_equiv_zero' _ hf,
-  by simp [hf, hg, norm]
+  by simp only [hf, hg, norm, dif_pos, zero_mul]
 else if hg : g ≈ 0 then
   have hf : f * g ≈ 0, from mul_equiv_zero _ hg,
-  by simp [hf, hg, norm]
+  by simp only [hf, hg, norm, dif_pos, mul_zero]
 else
   have hfg : ¬ f * g ≈ 0, by apply mul_not_equiv_zero; assumption,
   begin
@@ -357,11 +357,11 @@ end
 theorem norm_nonarchimedean (f g : padic_seq p) : (f + g).norm ≤ max (f.norm) (g.norm) :=
 if hfg : f + g ≈ 0 then
   have 0 ≤ max (f.norm) (g.norm), from le_max_left_of_le (norm_nonneg _),
-  by simpa [hfg, norm]
+  by simpa only [hfg, norm, ne.def, le_max_iff, cau_seq.add_apply, not_true, dif_pos]
 else if hf : f ≈ 0 then
   have hfg' : f + g ≈ g,
   { change lim_zero (f - 0) at hf,
-    show lim_zero (f + g - g), by simpa using hf },
+    show lim_zero (f + g - g), by simpa only [sub_zero, add_sub_cancel] using hf },
   have hcfg : (f + g).norm = g.norm, from norm_equiv hfg',
   have hcl : f.norm = 0, from (norm_zero_iff f).2 hf,
   have max (f.norm) (g.norm) = g.norm,
@@ -370,7 +370,7 @@ else if hf : f ≈ 0 then
 else if hg : g ≈ 0 then
   have hfg' : f + g ≈ f,
   { change lim_zero (g - 0) at hg,
-    show lim_zero (f + g - f), by  simpa [add_sub_cancel'] using hg },
+    show lim_zero (f + g - f), by simpa only [add_sub_cancel', sub_zero] using hg },
   have hcfg : (f + g).norm = f.norm, from norm_equiv hfg',
   have hcl : g.norm = 0, from (norm_zero_iff g).2 hg,
   have max (f.norm) (g.norm) = f.norm,
@@ -382,11 +382,12 @@ lemma norm_eq {f g : padic_seq p} (h : ∀ k, padic_norm p (f k) = padic_norm p
   f.norm = g.norm :=
 if hf : f ≈ 0 then
   have hg : g ≈ 0, from equiv_zero_of_val_eq_of_equiv_zero h hf,
-  by simp [hf, hg, norm]
+  by simp only [hf, hg, norm, dif_pos]
 else
-  have hg : ¬ g ≈ 0, from λ hg, hf $ equiv_zero_of_val_eq_of_equiv_zero (by simp [h]) hg,
+  have hg : ¬ g ≈ 0, from λ hg, hf $ equiv_zero_of_val_eq_of_equiv_zero
+    (by simp only [h, forall_const, eq_self_iff_true]) hg,
   begin
-    simp [hg, hf, norm],
+    simp only [hg, hf, norm, dif_neg, not_false_iff],
     let i := max (stationary_point hf) (stationary_point hg),
     have hpf : padic_norm p (f (stationary_point hf)) = padic_norm p (f i),
     { apply stationary_point_spec, apply le_max_left, apply le_refl },
@@ -400,31 +401,30 @@ norm_eq $ by simp
 
 lemma norm_eq_of_add_equiv_zero {f g : padic_seq p} (h : f + g ≈ 0) : f.norm = g.norm :=
 have lim_zero (f + g - 0), from h,
-have f ≈ -g, from show lim_zero (f - (-g)), by simpa,
+have f ≈ -g, from show lim_zero (f - (-g)), by simpa only [sub_zero, sub_neg_eq_add],
 have f.norm = (-g).norm, from norm_equiv this,
-by simpa [norm_neg] using this
+by simpa only [norm_neg] using this
 
 lemma add_eq_max_of_ne {f g : padic_seq p} (hfgne : f.norm ≠ g.norm) :
   (f + g).norm = max f.norm g.norm :=
 have hfg : ¬f + g ≈ 0, from mt norm_eq_of_add_equiv_zero hfgne,
 if hf : f ≈ 0 then
   have lim_zero (f - 0), from hf,
-  have f + g ≈ g, from show lim_zero ((f + g) - g), by simpa,
+  have f + g ≈ g, from show lim_zero ((f + g) - g), by simpa only [sub_zero, add_sub_cancel],
   have h1 : (f+g).norm = g.norm, from norm_equiv this,
   have h2 : f.norm = 0, from (norm_zero_iff _).2 hf,
   by rw [h1, h2]; rw max_eq_right (norm_nonneg _)
 else if hg : g ≈ 0 then
   have lim_zero (g - 0), from hg,
-  have f + g ≈ f, from show lim_zero ((f + g) - f), by rw [add_sub_cancel']; simpa,
+  have f + g ≈ f, from show lim_zero ((f + g) - f), by rw [add_sub_cancel']; simpa only [sub_zero],
   have h1 : (f+g).norm = f.norm, from norm_equiv this,
   have h2 : g.norm = 0, from (norm_zero_iff _).2 hg,
   by rw [h1, h2]; rw max_eq_left (norm_nonneg _)
 else
 begin
   unfold norm at ⊢ hfgne, split_ifs at ⊢ hfgne,
   padic_index_simp [hfg, hf, hg] at ⊢ hfgne,
-  apply padic_norm.add_eq_max_of_ne,
-  simpa [hf, hg, norm] using hfgne
+  exact padic_norm.add_eq_max_of_ne p hfgne
 end
 
 end embedding
@@ -547,7 +547,7 @@ begin
   by_contradiction h,
   cases cauchy₂ f hε with N hN,
   have : ∀ N, ∃ i ≥ N, ε ≤ (f - const _ (f i)).norm,
-    by simpa [not_forall] using h,
+    by simpa only [not_forall, not_exists, not_lt] using h,
   rcases this N with ⟨i, hi, hge⟩,
   have hne : ¬ (f - const (padic_norm p) (f i)) ≈ 0,
   { intro h, unfold padic_seq.norm at hge; split_ifs at hge, exact not_lt_of_ge hge hε },
@@ -650,7 +650,8 @@ quotient.induction_on q $ λ q',
         have := stationary_point_spec hne',
         cases decidable.em (stationary_point hne' ≤ N) with hle hle,
         { have := eq.symm (this (le_refl _) hle),
-          simp at this, simpa [this] },
+          simp only [const_apply, sub_apply, padic_norm.zero, sub_self] at this,
+          simpa only [this] },
         { apply hN,
           apply le_of_lt, apply lt_of_not_ge, apply hle, apply le_refl }}
     end⟩
@@ -661,6 +662,8 @@ open classical
 private lemma div_nat_pos (n : ℕ) : 0 < (1 / ((n + 1): ℚ)) :=
 div_pos zero_lt_one (by exact_mod_cast succ_pos _)
 
+/-- `lim_seq f`, for `f` a Cauchy sequence of `p`-adic numbers,
+is a sequence of rationals with the same limit point as `f`. -/
 def lim_seq : ℕ → ℚ := λ n, classical.some (rat_dense' (f n) (div_nat_pos n))
 
 lemma exi_rat_seq_conv {ε : ℚ} (hε : 0 < ε) :
@@ -683,19 +686,20 @@ let ⟨N, hN⟩ := exi_rat_seq_conv f hε3,
 begin
   existsi max N N2,
   intros j hj,
-  suffices : padic_norm_e ((↑(lim_seq f j) - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
+  suffices :
+    padic_norm_e ((↑(lim_seq f j) - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
   { ring at this ⊢,
     rw [← padic_norm_e.eq_padic_norm', ← padic.cast_eq_of_rat],
     exact_mod_cast this },
   { apply lt_of_le_of_lt,
     { apply padic_norm_e.add },
     { have : (3 : ℚ) ≠ 0, by norm_num,
       have : ε = ε / 3 + ε / 3 + ε / 3,
-      { field_simp [this], simp [bit0, bit1, mul_add] },
+      { field_simp [this], simp only [bit0, bit1, mul_add, mul_one] },
       rw this,
       apply add_lt_add,
       { suffices : padic_norm_e ((↑(lim_seq f j) - f j) + (f j - f (max N N2))) < ε / 3 + ε / 3,
-          by simpa [sub_add_sub_cancel],
+          by simpa only [sub_add_sub_cancel],
         apply lt_of_le_of_lt,
         { apply padic_norm_e.add },
         { apply add_lt_add,
@@ -851,6 +855,9 @@ protected lemma is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ∥q∥ = ↑q' :=
 if h : q = 0 then ⟨0, by simp [h]⟩
 else let ⟨n, hn⟩ := padic_norm_e.image h in ⟨_, hn⟩
 
+/--`rat_norm q`, for a `p`-adic number `q` is the `p`-adic norm of `q`, as rational number.
+
+The lemma `padic_norm_e.eq_rat_norm` asserts `∥q∥ = rat_norm q`. -/
 def rat_norm (q : ℚ_[p]) : ℚ := classical.some (padic_norm_e.is_rat q)
 
 lemma eq_rat_norm (q : ℚ_[p]) : ∥q∥ = rat_norm q := classical.some_spec (padic_norm_e.is_rat q)