Update HardyLittlewood.lean

fpvandoorn · Jul 31, 2024 · 06fa19b · 06fa19b
1 parent dddf0d6
commit 06fa19b
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean
@@ -100,8 +100,7 @@ theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall'' {α ι
     intro a ha
     rcases hu a ha with ⟨b, bu, hb, rb⟩
     refine ⟨b, bu, ?_⟩
-    have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
-    linarith
+    linarith [dist_le_add_of_nonempty_closedBall_inter_closedBall hb]
   have Ac : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) := by
     intro a ha
     rcases A a ha with ⟨b, bu, hb⟩