From bb076790b613ec8bbb0869bee7a6d5d010669df7 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 30 Jul 2024 10:55:22 +0200
Subject: [PATCH] Golf Helper.lean (#100)

---
 Carleson/Classical/Helper.lean | 31 +++++++++++--------------------
 1 file changed, 11 insertions(+), 20 deletions(-)

diff --git a/Carleson/Classical/Helper.lean b/Carleson/Classical/Helper.lean
index be798744..01b74c83 100644
--- a/Carleson/Classical/Helper.lean
+++ b/Carleson/Classical/Helper.lean
@@ -1,27 +1,23 @@
 import Carleson.ToMathlib.Misc
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 
-
 /-The lemmas in this file might either already exist in mathlib or be candidates to go there
   (in a generalized form).
 -/
 
-
 lemma intervalIntegral.integral_conj' {μ : MeasureTheory.Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}:
     ∫ x in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ x in a..b, f x ∂μ) := by
   rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,
-      RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul]
-  simp
+      RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul, RCLike.conj_ofReal]
 
 lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ x, ‖g x‖ ≤ δ) : IntervalIntegrable g MeasureTheory.volume a b := by
   apply @IntervalIntegrable.mono_fun' _ _ _ _ _ _ (fun _ ↦ δ)
-  apply intervalIntegrable_const
-  exact measurable_g.aestronglyMeasurable
-  rw [Filter.EventuallyLE, ae_restrict_iff_subtype measurableSet_uIoc]
-  apply Filter.eventually_of_forall
-  simp only [Subtype.forall]
-  intro x _
-  exact bddg x
+  · exact intervalIntegrable_const
+  · exact measurable_g.aestronglyMeasurable
+  · rw [Filter.EventuallyLE, ae_restrict_iff_subtype measurableSet_uIoc]
+    apply Filter.eventually_of_forall
+    rw [Subtype.forall]
+    exact fun x _ ↦ bddg x
 
 lemma IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
     (hg : IntervalIntegrable g μ a b) (hm : MeasureTheory.AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
@@ -32,15 +28,12 @@ lemma IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ 
 lemma IntervalIntegrable.mul_bdd {F : Type} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
     (hf : IntervalIntegrable f μ a b) (hm : MeasureTheory.AEStronglyMeasurable g μ) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
   conv => pattern (fun x ↦ f x * g x); ext x; rw [mul_comm]
-  apply hf.bdd_mul hm hgbdd
+  exact hf.bdd_mul hm hgbdd
 
 lemma MeasureTheory.IntegrableOn.sub {α : Type} {β : Type} {m : MeasurableSpace α}
     {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by
   apply MeasureTheory.Integrable.sub <;> rwa [← IntegrableOn]
 
-
-
-
 lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLinearOrder α] {ι : Type} [Nonempty ι]
     {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) :
     a ≤ ⨆ i ∈ s, f i := by
@@ -73,8 +66,6 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLi
   rw [iSup]
   convert csSup_singleton _
   rw [Set.eq_singleton_iff_unique_mem]
-  refine ⟨?_, fun x hx ↦ ?_⟩
-  · simp
-    use hi, fia
-  · simp at hx
-    rwa [hx.2] at fia
+  refine ⟨⟨hi, fia⟩, fun x hx ↦ ?_⟩
+  simp only [Set.mem_range, exists_prop] at hx
+  rwa [hx.2] at fia