chore(MeasureTheory): golf (#6641)

- Golf some proofs.
- Rename `MeasureTheory.indicatorConst_empty`
  to `MeasureTheory.indicatorConstLp_empty`.
- Change some linebreaks.

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -460,7 +460,7 @@ theorem integrable_condexpIndSMul (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs
 
 theorem condexpIndSMul_empty {x : G} : condexpIndSMul hm MeasurableSet.empty
     ((@measure_empty _ _ μ).le.trans_lt ENNReal.coe_lt_top).ne x = 0 := by
-  rw [condexpIndSMul, indicatorConst_empty]
+  rw [condexpIndSMul, indicatorConstLp_empty]
   simp only [Submodule.coe_zero, ContinuousLinearMap.map_zero]
 #align measure_theory.condexp_ind_smul_empty MeasureTheory.condexpIndSMul_empty
 

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -774,13 +774,13 @@ theorem norm_indicatorConstLp_le :
   exact ENNReal.rpow_ne_top_of_nonneg (by positivity) hμs
 
 @[simp]
-theorem indicatorConst_empty :
+theorem indicatorConstLp_empty :
     indicatorConstLp p MeasurableSet.empty (by simp : μ ∅ ≠ ∞) c = 0 := by
   rw [Lp.eq_zero_iff_ae_eq_zero]
   convert indicatorConstLp_coeFn (E := E)
   simp [Set.indicator_empty']
   rfl
-#align measure_theory.indicator_const_empty MeasureTheory.indicatorConst_empty
+#align measure_theory.indicator_const_empty MeasureTheory.indicatorConstLp_empty
 
 theorem memℒp_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g))
     (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
@@ -794,10 +794,7 @@ theorem memℒp_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (supp
 /-- The indicator of a disjoint union of two sets is the sum of the indicators of the sets. -/
 theorem indicatorConstLp_disjoint_union {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t)
     (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) (hst : s ∩ t = ∅) (c : E) :
-    indicatorConstLp p (hs.union ht)
-        ((measure_union_le s t).trans_lt
-            (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne
-        c =
+    indicatorConstLp p (hs.union ht) (measure_union_ne_top hμs hμt) c =
       indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c := by
   ext1
   refine' indicatorConstLp_coeFn.trans (EventuallyEq.trans _ (Lp.coeFn_add _ _).symm)

Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

@@ -61,7 +61,6 @@ namespace SimpleFunc
 
 /-! ### Lp approximation by simple functions -/
 
-
 section Lp
 
 variable [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [NormedAddCommGroup F]
@@ -204,9 +203,8 @@ theorem _root_.MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt {E : Type*}
     {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ g : β →ₛ E, snorm (f - ⇑g) p μ < ε ∧ Memℒp g p μ := by
   borelize E
   let f' := hf.1.mk f
-  suffices H : ∃ g : β →ₛ E, snorm (f' - ⇑g) p μ < ε ∧ Memℒp g p μ
-  · rcases H with ⟨g, hg, g_mem⟩
-    refine' ⟨g, _, g_mem⟩
+  rsuffices ⟨g, hg, g_mem⟩ : ∃ g : β →ₛ E, snorm (f' - ⇑g) p μ < ε ∧ Memℒp g p μ
+  · refine' ⟨g, _, g_mem⟩
     suffices snorm (f - ⇑g) p μ = snorm (f' - ⇑g) p μ by rwa [this]
     apply snorm_congr_ae
     filter_upwards [hf.1.ae_eq_mk] with x hx
@@ -215,9 +213,8 @@ theorem _root_.MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt {E : Type*}
   have f'meas : Measurable f' := hf.1.measurable_mk
   have : SeparableSpace (range f' ∪ {0} : Set E) :=
     StronglyMeasurable.separableSpace_range_union_singleton hf.1.stronglyMeasurable_mk
-  rcases((tendsto_order.1 (tendsto_approxOn_range_Lp_snorm hp_ne_top f'meas hf'.2)).2 ε
-        hε.bot_lt).exists with
-    ⟨n, hn⟩
+  rcases ((tendsto_approxOn_range_Lp_snorm hp_ne_top f'meas hf'.2).eventually <|
+    gt_mem_nhds hε.bot_lt).exists with ⟨n, hn⟩
   rw [← snorm_neg, neg_sub] at hn
   exact ⟨_, hn, memℒp_approxOn_range f'meas hf' _⟩
 #align measure_theory.mem_ℒp.exists_simple_func_snorm_sub_lt MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt
@@ -835,45 +832,15 @@ theorem coeFn_zero : (0 : Lp.simpleFunc G p μ) =ᵐ[μ] (0 : α → G) :=
 variable {p μ G}
 
 theorem coeFn_nonneg (f : Lp.simpleFunc G p μ) : (0 : α → G) ≤ᵐ[μ] f ↔ 0 ≤ f := by
-  rw [← Lp.simpleFunc.coeFn_le]
-  have h0 : (0 : Lp.simpleFunc G p μ) =ᵐ[μ] (0 : α → G) := Lp.simpleFunc.coeFn_zero p μ G
-  constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2
-  · rwa [h2]
-  · rwa [← h2]
+  rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]
 #align measure_theory.Lp.simple_func.coe_fn_nonneg MeasureTheory.Lp.simpleFunc.coeFn_nonneg
 
 theorem exists_simpleFunc_nonneg_ae_eq {f : Lp.simpleFunc G p μ} (hf : 0 ≤ f) :
     ∃ f' : α →ₛ G, 0 ≤ f' ∧ f =ᵐ[μ] f' := by
-  rw [← Lp.simpleFunc.coeFn_nonneg] at hf
-  have hf_ae : 0 ≤ᵐ[μ] simpleFunc.toSimpleFunc f := by
-    filter_upwards [toSimpleFunc_eq_toFun f, hf] with _ h1 _; rwa [h1]
-  let s := (toMeasurable μ { x | ¬0 ≤ simpleFunc.toSimpleFunc f x })ᶜ
-  have hs_zero : μ sᶜ = 0 := by
-    rw [compl_compl, measure_toMeasurable]; rwa [EventuallyLE, ae_iff] at hf_ae
-  have hfs_nonneg : ∀ x ∈ s, 0 ≤ simpleFunc.toSimpleFunc f x := by
-    intro x hxs
-    rw [mem_compl_iff] at hxs
-    have hx' : x ∉ { a : α | ¬0 ≤ simpleFunc.toSimpleFunc f a } := fun h =>
-      hxs (subset_toMeasurable μ _ h)
-    rwa [Set.nmem_setOf_iff, Classical.not_not] at hx'
-  let f' :=
-    SimpleFunc.piecewise s (measurableSet_toMeasurable μ _).compl (simpleFunc.toSimpleFunc f)
-      (SimpleFunc.const α (0 : G))
-  refine' ⟨f', fun x => _, _⟩
-  · rw [SimpleFunc.piecewise_apply]
-    by_cases hxs : x ∈ s
-    · simp only [hxs, hfs_nonneg x hxs, if_true, Pi.zero_apply, SimpleFunc.coe_zero]
-    · simp only [hxs, SimpleFunc.const_zero, if_false]; rfl
-  · rw [SimpleFunc.coe_piecewise]
-    have : s =ᵐ[μ] univ := by
-      rw [ae_eq_set]
-      simp only [true_and_iff, measure_empty, eq_self_iff_true, diff_univ, ← compl_eq_univ_diff]
-      exact hs_zero
-    refine' EventuallyEq.trans (toSimpleFunc_eq_toFun f).symm _
-    refine' EventuallyEq.trans _ (piecewise_ae_eq_of_ae_eq_set this.symm)
-    letI : DecidablePred (· ∈ (univ : Set α)) := fun _ => Classical.propDecidable _
-    simp only [SimpleFunc.const_zero, indicator_univ, piecewise_eq_indicator, SimpleFunc.coe_zero]
-    rfl
+  rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩
+  change 0 ≤ᵐ[μ] g at hf
+  refine ⟨g ⊔ 0, le_sup_right, (AEEqFun.coeFn_mk _ _).trans ?_⟩
+  exact hf.mono fun x hx ↦ (sup_of_le_left hx).symm
 #align measure_theory.Lp.simple_func.exists_simple_func_nonneg_ae_eq MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq
 
 variable (p μ G)
@@ -884,9 +851,8 @@ def coeSimpleFuncNonnegToLpNonneg :
 #align measure_theory.Lp.simple_func.coe_simple_func_nonneg_to_Lp_nonneg MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg
 
 theorem denseRange_coeSimpleFuncNonnegToLpNonneg [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) :
-    DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G) := by
+    DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G) := fun g ↦ by
   borelize G
-  intro g
   rw [mem_closure_iff_seq_limit]
   have hg_memℒp : Memℒp (g : α → G) p μ := Lp.memℒp (g : Lp G p μ)
   have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } := by
@@ -957,15 +923,10 @@ suffices to show that
 -/
 @[elab_as_elim]
 theorem Lp.induction [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) (P : Lp E p μ → Prop)
-    (h_ind :
-      ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞),
-        P (Lp.simpleFunc.indicatorConst p hs hμs.ne c))
-    (h_add :
-      ∀ ⦃f g⦄,
-        ∀ hf : Memℒp f p μ,
-          ∀ hg : Memℒp g p μ,
-            Disjoint (support f) (support g) →
-              P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g))
+    (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞),
+      P (Lp.simpleFunc.indicatorConst p hs hμs.ne c))
+    (h_add : ∀ ⦃f g⦄, ∀ hf : Memℒp f p μ, ∀ hg : Memℒp g p μ, Disjoint (support f) (support g) →
+      P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g))
     (h_closed : IsClosed { f : Lp E p μ | P f }) : ∀ f : Lp E p μ, P f := by
   refine' fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f h_closed _
   refine' Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne'
@@ -989,9 +950,8 @@ of their images is a subset of `{0}`).
 @[elab_as_elim]
 theorem Memℒp.induction [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop)
     (h_ind : ∀ (c : E) ⦃s⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun _ => c))
-    (h_add :
-      ∀ ⦃f g : α → E⦄,
-        Disjoint (support f) (support g) → Memℒp f p μ → Memℒp g p μ → P f → P g → P (f + g))
+    (h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p μ → Memℒp g p μ →
+      P f → P g → P (f + g))
     (h_closed : IsClosed { f : Lp E p μ | P f })
     (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → Memℒp f p μ → P f → P g) :
     ∀ ⦃f : α → E⦄, Memℒp f p μ → P f := by