perf(analysis/calculus/specific_functions): speed up `exp_neg_inv_glu…

…e.f_aux_deriv` (#16812)

This caused some [bors failures](https://github.com/leanprover-community/mathlib/actions/runs/3182965873/jobs/5189596416) yesterday. The new proof features a 8x time reduction from >20s to <2.5s on my machine.

src/analysis/calculus/specific_functions.lean

@@ -64,7 +64,7 @@ derivatives for `x > 0`. The `n`-th derivative is of the form `P_aux n (x) exp(-
 where `P_aux n` is computed inductively. -/
 noncomputable def P_aux : ℕ → polynomial ℝ
 | 0 := 1
-| (n+1) := X^2 * (P_aux n).derivative  + (1 - C ↑(2 * n) * X) * (P_aux n)
+| (n+1) := X^2 * (P_aux n).derivative + (1 - C ↑(2 * n) * X) * (P_aux n)
 
 /-- Formula for the `n`-th derivative of `exp_neg_inv_glue`, as an auxiliary function `f_aux`. -/
 def f_aux (n : ℕ) (x : ℝ) : ℝ :=
@@ -86,13 +86,16 @@ lemma f_aux_deriv (n : ℕ) (x : ℝ) (hx : x ≠ 0) :
   has_deriv_at (λx, (P_aux n).eval x * exp (-x⁻¹) / x^(2 * n))
     ((P_aux (n+1)).eval x * exp (-x⁻¹) / x^(2 * (n + 1))) x :=
 begin
-  have A : ∀ k : ℕ, 2 * (k + 1) - 1 = 2 * k + 1 := λ k, rfl,
+  simp only [P_aux, eval_add, eval_sub, eval_mul, eval_pow, eval_X, eval_C, eval_one],
   convert (((P_aux n).has_deriv_at x).mul
                (((has_deriv_at_exp _).comp x (has_deriv_at_inv hx).neg))).div
             (has_deriv_at_pow (2 * n) x) (pow_ne_zero _ hx) using 1,
-  field_simp [hx, P_aux],
-  -- `ring_exp` can't solve `p ∨ q` goal generated by `mul_eq_mul_right_iff`
-  cases n; simp [nat.succ_eq_add_one, A, -mul_eq_mul_right_iff]; ring_exp
+  rw div_eq_div_iff,
+  { have := pow_ne_zero 2 hx, field_simp only,
+    cases n,
+    { simp only [mul_zero, nat.cast_zero, mul_one], ring },
+    { rw (id rfl : 2 * n.succ - 1 = 2 * n + 1), ring_exp } },
+  all_goals { apply_rules [pow_ne_zero] },
 end
 
 /-- For positive values, the derivative of the `n`-th auxiliary function `f_aux n`