chore(*): don't use tactic internal lemmas in proofs (#11641)

Some lemmas that are intended as internals to a tactic get picked up by library search and end up in proofs.
We replace a few of these tactic lemma uses with actual library lemmas which should be more maintainable, de-coupling tactic internals from the actual library.

src/analysis/mean_inequalities.lean

@@ -306,8 +306,8 @@ begin
   { simp_rw [f', g', div_mul_div, ← sum_div] at this,
     rwa [div_le_iff, one_mul] at this,
     refine mul_ne_zero _ _,
-    { rw [ne.def, rpow_eq_zero_iff, auto.not_and_eq], exact or.inl hF_zero, },
-    { rw [ne.def, rpow_eq_zero_iff, auto.not_and_eq], exact or.inl hG_zero, }, },
+    { rw [ne.def, rpow_eq_zero_iff, not_and_distrib], exact or.inl hF_zero, },
+    { rw [ne.def, rpow_eq_zero_iff, not_and_distrib], exact or.inl hG_zero, }, },
   refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq _) (le_of_eq _),
   { simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel hpq.ne_zero, rpow_one,
       div_self hF_zero], },

src/analysis/special_functions/trigonometric/basic.lean

@@ -826,8 +826,8 @@ lemma tendsto_cos_pi_div_two : tendsto cos (𝓝[<] (π/2)) (𝓝[>] 0) :=
 begin
   apply tendsto_nhds_within_of_tendsto_nhds_of_eventually_within,
   { convert continuous_cos.continuous_within_at, simp },
-  { filter_upwards [Ioo_mem_nhds_within_Iio (right_mem_Ioc.mpr (norm_num.lt_neg_pos
-      _ _ pi_div_two_pos pi_div_two_pos))] with x hx using cos_pos_of_mem_Ioo hx },
+  { filter_upwards [Ioo_mem_nhds_within_Iio (right_mem_Ioc.mpr (neg_lt_self pi_div_two_pos))]
+      with x hx using cos_pos_of_mem_Ioo hx },
 end
 
 lemma tendsto_tan_pi_div_two : tendsto tan (𝓝[<] (π/2)) at_top :=
@@ -844,8 +844,8 @@ lemma tendsto_cos_neg_pi_div_two : tendsto cos (𝓝[>] (-(π/2))) (𝓝[>] 0) :
 begin
   apply tendsto_nhds_within_of_tendsto_nhds_of_eventually_within,
   { convert continuous_cos.continuous_within_at, simp },
-  { filter_upwards [Ioo_mem_nhds_within_Ioi (left_mem_Ico.mpr (norm_num.lt_neg_pos
-      _ _ pi_div_two_pos pi_div_two_pos))] with x hx using cos_pos_of_mem_Ioo hx },
+  { filter_upwards [Ioo_mem_nhds_within_Ioi (left_mem_Ico.mpr (neg_lt_self pi_div_two_pos))]
+      with x hx using cos_pos_of_mem_Ioo hx },
 end
 
 lemma tendsto_tan_neg_pi_div_two : tendsto tan (𝓝[>] (-(π/2))) at_bot :=

src/data/nat/totient.lean

@@ -220,7 +220,7 @@ begin
       rw [totient_one, tsub_self] at h,
       exact one_ne_zero h } },
   rw [totient_eq_card_coprime, range_eq_Ico, ←Ico_insert_succ_left hp.le, finset.filter_insert,
-    if_neg (tactic.norm_num.nat_coprime_helper_zero_right p hp), ←nat.card_Ico 1 p] at h,
+      if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ←nat.card_Ico 1 p] at h,
   refine p.prime_of_coprime hp (λ n hn hnz, finset.filter_card_eq h n $ finset.mem_Ico.mpr ⟨_, hn⟩),
   rwa [succ_le_iff, pos_iff_ne_zero],
 end

src/data/real/pi/leibniz.lean

@@ -103,7 +103,7 @@ begin
   have f'_bound : ∀ x ∈ Icc (-1:ℝ) 1, |f' x| ≤ |x|^(2*k),
   { intros x hx,
     rw [abs_div, is_absolute_value.abv_pow abs (-x^2) k, abs_neg, is_absolute_value.abv_pow abs x 2,
-       tactic.ring_exp.pow_e_pf_exp rfl rfl],
+        ← pow_mul],
     refine div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _,
     refine le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _,
     rw abs_of_nonneg ((add_nonneg zero_le_one (sq_nonneg x)) : (0 : ℝ) ≤ _),

src/data/set/lattice.lean

@@ -52,7 +52,7 @@ In lemma names,
 * `⋂₀`: `set.sInter`
 -/
 
-open function tactic set auto
+open function tactic set
 
 universes u
 variables {α β γ : Type*} {ι ι' ι₂ : Sort*} {κ κ₁ κ₂ : ι → Sort*} {κ' : ι' → Sort*}

src/field_theory/splitting_field.lean

@@ -395,7 +395,7 @@ begin
     simp only [nat_degree_mul (ne_zero_of_monic hprodmonic) qzero] },
   have degq : q.nat_degree = 0,
   { rw hdegree at degp,
-    exact (add_right_inj p.nat_degree).mp (tactic.ring_exp.add_pf_sum_z degp rfl).symm },
+    rw [← add_right_inj p.nat_degree, ← degp, add_zero], },
   obtain ⟨u, hu⟩ := is_unit_iff_degree_eq_zero.2 ((degree_eq_iff_nat_degree_eq qzero).2 degq),
   have hassoc : associated (multiset.map (λ (a : K), X - C a) p.roots).prod p,
   { rw associated, use u, rw [hu, ← hq] },

src/measure_theory/function/lp_space.lean

@@ -278,7 +278,7 @@ begin
     rw ←ennreal.rpow_mul,
     suffices hp_cancel : q * (1/q) = 1, by rw [hp_cancel, ennreal.rpow_one],
     rw [one_div, mul_inv_cancel hq_ne_zero], },
-  { rw [ne.def, ennreal.rpow_eq_top_iff, auto.not_or_eq, auto.not_and_eq, auto.not_and_eq],
+  { rw [ne.def, ennreal.rpow_eq_top_iff, not_or_distrib, not_and_distrib, not_and_distrib],
     split,
     { left,
       rwa [ennreal.coe_eq_zero, nnnorm_eq_zero], },

src/measure_theory/integral/set_to_l1.lean

@@ -1704,7 +1704,7 @@ begin
   refine set_to_fun_measure_zero' hT (λ s hs hμs, _),
   rw lt_top_iff_ne_top at hμs,
   simp only [true_and, measure.smul_apply, with_top.mul_eq_top_iff, eq_self_iff_true, top_ne_zero,
-    ne.def, not_false_iff, auto.not_or_eq, not_not] at hμs,
+    ne.def, not_false_iff, not_or_distrib, not_not] at hμs,
   simp only [hμs.right, measure.smul_apply, mul_zero],
 end
 

test/induction.lean

@@ -1288,7 +1288,7 @@ begin
       apply exists.intro s,
       exact small_step.seq_skip },
     case inr {
-      simp [h, auto.not_forall_eq, auto.not_not_eq] at ihS,
+      simp [h, not_forall, not_not] at ihS,
       cases' ihS s with S' hS',
       cases' hS' with s' hs',
       apply exists.intro (S' ;; T),