chore(measure_theory/decomposition/unsigned_hahn): speedup Hahn decom…

…position (#18419)

From 49s to 4s on my computer. The key point was to replace the super-slow `ac_refl` with `abel`.

src/measure_theory/decomposition/unsigned_hahn.lean

@@ -28,11 +28,6 @@ namespace measure_theory
 
 variables {α : Type*} [measurable_space α] {μ ν : measure α}
 
--- suddenly this is necessary?!
-private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
-  γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
-by linarith
-
 /-- **Hahn decomposition theorem** -/
 lemma hahn_decomposition [is_finite_measure μ] [is_finite_measure ν] :
   ∃s, measurable_set s ∧
@@ -61,7 +56,7 @@ begin
       ennreal.to_nnreal_add (hμ _) (hμ _), ennreal.to_nnreal_add (hν _) (hν _),
       nnreal.coe_add, nnreal.coe_add],
     simp only [sub_eq_add_neg, neg_add],
-    ac_refl },
+    abel },
 
   have d_Union : ∀(s : ℕ → set α), monotone s →
     tendsto (λn, d (s n)) at_top (𝓝 (d (⋃n, s n))),
@@ -127,7 +122,7 @@ begin
     { have := he₂ m,
       simp only [f],
       rw [nat.Ico_succ_singleton, finset.inf_singleton],
-      exact aux this },
+      linarith },
     { assume n (hmn : m ≤ n) ih,
       have : γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)),
       { calc γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n+1)) ≤
@@ -138,15 +133,15 @@ begin
             linarith
           end
           ... = (γ - (1 / 2)^(n+1)) + (γ - 2 * (1 / 2)^m + (1 / 2)^n) :
-            by simp only [sub_eq_add_neg]; ac_refl
+            by simp only [sub_eq_add_neg]; abel
           ... ≤ d (e (n + 1)) + d (f m n) : add_le_add (le_of_lt $ he₂ _) ih
           ... ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m (n + 1)) :
             by rw [f_succ _ _ hmn, d_split (f m n) (e (n + 1)) (hf _ _) (he₁ _), add_assoc]
           ... = d (e (n + 1) ∪ f m n) + d (f m (n + 1)) :
             begin
               rw [d_split (e (n + 1) ∪ f m n) (e (n + 1)),
                 union_diff_left, union_inter_cancel_left],
-              ac_refl,
+              abel,
               exact (he₁ _).union (hf _ _),
               exact (he₁ _)
             end
@@ -157,7 +152,8 @@ begin
   let s := ⋃ m, ⋂n, f m n,
   have γ_le_d_s : γ ≤ d s,
   { have hγ : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 γ),
-    { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 (γ - 2 * 0)), { simpa },
+    { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 (γ - 2 * 0)),
+      { simpa only [mul_zero, tsub_zero] },
       exact (tendsto_const_nhds.sub $ tendsto_const_nhds.mul $
         tendsto_pow_at_top_nhds_0_of_lt_1
           (le_of_lt $ half_pos $ zero_lt_one) (half_lt_self zero_lt_one)) },