fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3…

….6s to 180ms (#11426)

The timings are measured for the single small begin/end block. The proof as a whole is still around 7.6s, down from 11s.

The fault here was likely the `convert`, which presumably spent a lot of time trying to unify typeclass arguments.

src/analysis/calculus/fderiv_symmetric.lean

@@ -157,10 +157,7 @@ begin
       { refine ⟨_, xt_mem t ⟨ht.1, ht.2.le⟩⟩,
         rw [add_assoc, add_mem_ball_iff_norm],
         exact I.trans_lt hδ },
-      have := sδ H,
-      simp only [mem_set_of_eq] at this,
-      convert this;
-      abel
+      simpa only [mem_set_of_eq, add_assoc x, add_sub_cancel'] using sδ H,
     end
     ... ≤ (ε * (∥h • v∥ + ∥h • w∥)) * (∥h • w∥) :
     begin