diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
index ce6c2b97efec91..542a9db3d2c2a9 100644
--- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
+++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
@@ -111,25 +111,20 @@ theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty
   inhabit ι
   rcases eq_or_neBot L with (rfl | hL)
   · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
-  let p : α → (ι → β) → Prop := fun x f' => ∃ l : β, Tendsto (fun n => f' n) L (𝓝 l)
-  have hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x := fun x hx =>
-    aeSeq.fun_prop_of_mem_aeSeqSet hf hx
-  have h_ae_eq : ∀ᵐ x ∂μ, ∀ n, aeSeq hf p n x = f n x := aeSeq.aeSeq_eq_fun_ae hf h_ae_tendsto
-  set f_lim : α → β := fun x => dite (x ∈ aeSeqSet hf p) (fun h => (hp_mem x h).choose)
-    fun _ => (⟨f default x⟩ : Nonempty β).some
-  have hf_lim : ∀ x, Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x)) := by
-    intro x
-    simp only [aeSeq, f_lim]
-    split_ifs with h
-    · refine (hp_mem x h).choose_spec.congr fun n => ?_
-      exact (aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h n).symm
-    · exact tendsto_const_nhds
-  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) :=
-    h_ae_eq.mono fun x hx => (hf_lim x).congr hx
-  have h_f_lim_meas : Measurable f_lim :=
-    measurable_of_tendsto_metrizable' L (aeSeq.measurable hf p)
-      (tendsto_pi_nhds.mpr fun x => hf_lim x)
-  exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩
+  letI := hL
+  let f_lim : α → β := fun x =>
+    if h : ∃ l : β, Tendsto (fun n => f n x) L (𝓝 l) then
+      h.choose
+    else
+      (⟨f default x⟩ : Nonempty β).some
+  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) := by
+    filter_upwards [h_ae_tendsto] with x hx
+    simpa [f_lim, hx] using hx.choose_spec
+  have hf_lim : AEMeasurable f_lim μ :=
+    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
+  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
+  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
+  simpa [h_eq] using hx
 
 end Limits
 
diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
index d589bd06fe92b3..e053d72add64ca 100644
--- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
+++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
@@ -494,25 +494,17 @@ lemma measurable_of_real_real {f : EReal × EReal → β}
   · exact measurable_of_measurable_real h_top_left
 
 private lemma measurable_const_mul (c : EReal) : Measurable fun (x : EReal) ↦ c * x := by
-  refine measurable_of_measurable_real ?_
-  have h1 : (fun (p : ℝ) ↦ (⊥ : EReal) * p)
-      = fun p ↦ if p = 0 then (0 : EReal) else (if p < 0 then ⊤ else ⊥) := by
-    ext p
-    split_ifs with h1 h2
-    · simp [h1]
-    · rw [bot_mul_coe_of_neg h2]
-    · rw [bot_mul_coe_of_pos]
-      exact lt_of_le_of_ne (not_lt.mp h2) (Ne.symm h1)
-  have h2 : Measurable fun (p : ℝ) ↦ if p = 0 then (0 : EReal) else if p < 0 then ⊤ else ⊥ := by
-    refine Measurable.piecewise (measurableSet_singleton _) measurable_const ?_
-    exact Measurable.piecewise measurableSet_Iio measurable_const measurable_const
-  induction c with
-  | bot => rwa [h1]
-  | coe c => exact (measurable_id.const_mul _).coe_real_ereal
-  | top =>
-    simp_rw [← neg_bot, neg_mul]
-    apply Measurable.neg
-    rwa [h1]
+  rcases eq_or_ne c 0 with rfl | hc
+  · simpa only [zero_mul] using (measurable_const : Measurable fun _ : EReal => (0 : EReal))
+  · refine measurable_of_continuousOn_compl_singleton 0 ?_
+    intro x hx
+    have hx0 : x ≠ 0 := by simpa using hx
+    have hcont : ContinuousAt (fun x : EReal ↦ c * x) x :=
+      ContinuousAt.comp_of_eq (g := fun p : EReal × EReal ↦ p.1 * p.2) (f := fun x ↦ (c, x))
+        (y := (c, x))
+        (EReal.continuousAt_mul (p := (c, x)) (Or.inl hc) (Or.inl hc) (Or.inr hx0) (Or.inr hx0))
+        (continuousAt_const.prodMk continuousAt_id) rfl
+    exact hcont.continuousWithinAt
 
 instance : MeasurableMul₂ EReal := by
   refine ⟨measurable_of_real_real ?_ ?_ ?_ ?_ ?_⟩
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index 5f0f7f9209e3a2..1ad00cb7d6a5b2 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -450,23 +450,6 @@ theorem ae_eq_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s
     Set.pi I s =ᵐ[Measure.pi μ] Set.pi I t :=
   (ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le)
 
-lemma pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*}
-    [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
-    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e)
-      = Measure.pi μ := by
-  let e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) :=
-    MeasurableEquiv.piCongrLeft (fun i ↦ β i) e
-  refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm
-  rw [e_meas.measurableEmbedding.map_apply]
-  let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i)
-  have : e_meas ⁻¹' pi univ s = pi univ s' := by
-    ext x
-    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s']
-    refine (e.forall_congr ?_).symm
-    intro i
-    rw [MeasurableEquiv.piCongrLeft_apply_apply e x i]
-  simpa [this] using Fintype.prod_equiv _ (fun _ ↦ (μ _) (s' _)) _ (congrFun rfl)
-
 lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
     (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
     ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map
@@ -755,6 +738,12 @@ theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι
     MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume :=
   measurePreserving_piCongrLeft (fun _ ↦ volume) f
 
+lemma pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)]
+    (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
+    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) =
+      Measure.pi μ :=
+  (measurePreserving_piCongrLeft (α := fun i ↦ β i) (μ := μ) e).map_eq
+
 theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α]
     [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)]
     [∀ i, SigmaFinite (ν i)] :
diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
index d013f8556c1ebb..839012f57c07d2 100644
--- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
+++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
@@ -838,14 +838,10 @@ theorem MeasurableSet.image_of_measurable_injOn {f : γ → α}
   obtain ⟨t', t't, f_cont, t'_polish⟩ :
       ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
     f_meas.exists_continuous
-  have M : MeasurableSet[@borel γ t'] s :=
-    @Continuous.measurable γ γ t' (@borel γ t')
-      (@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl))
-      tγ _ _ _ (continuous_id_of_le t't) s hs
-  exact
-    @MeasurableSet.image_of_continuousOn_injOn γ
-      _ _ _ _ s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)
-      M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj
+  have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ]
+  letI : MeasurableSpace γ := @borel γ t'
+  letI : BorelSpace γ := ⟨rfl⟩
+  exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj
 
 /-- An injective continuous function on a Polish space is a measurable embedding. -/
 theorem Continuous.measurableEmbedding [BorelSpace β]
diff --git a/Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean b/Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
index ad67393a879f95..167836fbd0800b 100644
--- a/Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
+++ b/Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
@@ -39,14 +39,9 @@ theorem exists_subset_real_measurableEquiv : ∃ s : Set ℝ, MeasurableSet s 
   · cases finite_or_infinite α
     · obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
       refine ⟨_, ?_, h_nonempty_equiv⟩
-      letI : MeasurableSpace (Fin n) := borel (Fin n)
-      haveI : BorelSpace (Fin n) := ⟨rfl⟩
-      apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
-      exact continuous_of_discreteTopology.measurableEmbedding
-        (Nat.cast_injective.comp Fin.val_injective)
+      exact (Set.finite_range ((↑) : Fin n → ℝ)).measurableSet
     · refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
-      apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
-      exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective
+      exact Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet
   · refine
       ⟨univ, MeasurableSet.univ,
         ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
diff --git a/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean b/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean
index 339c14c20a1cf6..27cb9cd6f97bff 100644
--- a/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean
+++ b/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean
@@ -54,34 +54,23 @@ protected theorem limUnder [hE : Nonempty E] (hf : ∀ i, StronglyMeasurable (f
     StronglyMeasurable (fun x ↦ limUnder l (f · x)) := by
   obtain rfl | hl := eq_or_neBot l
   · simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const
-  borelize E
   let e := Classical.choice hE
-  rw [stronglyMeasurable_iff_measurable_separable]; constructor
-  · let conv := {x | ∃ c, Tendsto (f · x) l (𝓝 c)}
-    have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
-    have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
-        (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
-      ext x
-      by_cases hx : x ∈ conv
-      · rw [Function.extend_val_apply hx]
-      · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
-    rw [this]
-    refine (MeasurableEmbedding.subtype_coe mconv).measurable_extend
-      (measurable_of_tendsto_metrizable' l
-        (fun i ↦ (hf i).measurable.comp measurable_subtype_coe)
-        (tendsto_pi_nhds.2 fun ⟨x, ⟨c, hc⟩⟩ ↦ ?_)) measurable_const
+  let conv := {x | ∃ c, Tendsto (f · x) l (𝓝 c)}
+  have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
+  have hconv : StronglyMeasurable (fun x : conv ↦ limUnder l (f · x)) := by
+    refine stronglyMeasurable_of_tendsto l
+      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
+    refine tendsto_pi_nhds.2 fun x ↦ ?_
+    obtain ⟨c, hc⟩ := x.2
     rwa [hc.limUnder_eq]
-  · let s := closure (⋃ i, range (f i)) ∪ {e}
-    have hs : IsSeparable s := (IsSeparable.iUnion (fun i ↦ (hf i).isSeparable_range)).closure.union
-      (finite_singleton e).isSeparable
-    refine hs.mono ?_
-    rintro - ⟨x, rfl⟩
-    by_cases hx : ∃ c, Tendsto (f · x) l (𝓝 c)
-    · obtain ⟨c, hc⟩ := hx
-      simp_rw [hc.limUnder_eq]
-      exact subset_union_left <| mem_closure_of_tendsto hc
-        (Eventually.of_forall fun i ↦ mem_iUnion.2 ⟨i, ⟨x, rfl⟩⟩)
-    · simp_rw [limUnder_of_not_tendsto hx]
-      exact subset_union_right (mem_singleton e)
+  have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
+      (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
+    ext x
+    by_cases hx : x ∈ conv
+    · rw [Function.extend_val_apply hx]
+    · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
+  rw [this]
+  exact (MeasurableEmbedding.subtype_coe mconv).stronglyMeasurable_extend hconv
+    stronglyMeasurable_const
 
 end MeasureTheory.StronglyMeasurable
diff --git a/Mathlib/MeasureTheory/Covering/Besicovitch.lean b/Mathlib/MeasureTheory/Covering/Besicovitch.lean
index 0752545b875445..9504208d2a7aab 100644
--- a/Mathlib/MeasureTheory/Covering/Besicovitch.lean
+++ b/Mathlib/MeasureTheory/Covering/Besicovitch.lean
@@ -920,14 +920,10 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SFinite μ
   let r x := if x ∈ s' then r1 x else r0 x
   have r_t0 : ∀ x ∈ t0, r x = r0 x := by
     intro x hx
-    have : x ∉ s' := by
-      simp only [s', not_exists, exists_prop, mem_iUnion, mem_closedBall, not_and, not_lt, not_le,
-        mem_diff, not_forall]
-      intro _
-      refine ⟨x, hx, ?_⟩
-      rw [dist_self]
-      exact (hr0 x hx).2.1.le
-    simp only [r, if_neg this]
+    have hx_not_mem : x ∉ s' := fun hxs' =>
+      hxs'.2 <| mem_iUnion₂.2 ⟨x, hx, by
+        simpa [mem_closedBall] using (hr0 x hx).2.1.le⟩
+    simp [r, hx_not_mem]
   -- the desired covering set is given by the union of the families constructed in the first and
   -- second steps.
   refine ⟨t0 ∪ ⋃ i : Fin N, ((↑) : s' → α) '' S i, r, ?_, ?_, ?_, ?_, ?_⟩
diff --git a/Mathlib/MeasureTheory/Function/AEEqFun.lean b/Mathlib/MeasureTheory/Function/AEEqFun.lean
index 506c28877e204b..e67e6f90e383c3 100644
--- a/Mathlib/MeasureTheory/Function/AEEqFun.lean
+++ b/Mathlib/MeasureTheory/Function/AEEqFun.lean
@@ -573,23 +573,17 @@ instance instSup : Max (α →ₘ[μ] β) where max f g := AEEqFun.comp₂ (· 
 theorem coeFn_sup (f g : α →ₘ[μ] β) : ⇑(f ⊔ g) =ᵐ[μ] fun x => f x ⊔ g x :=
   coeFn_comp₂ _ _ _ _
 
-protected theorem le_sup_left (f g : α →ₘ[μ] β) : f ≤ f ⊔ g := by
-  rw [← coeFn_le]
-  filter_upwards [coeFn_sup f g] with _ ha
-  rw [ha]
-  exact le_sup_left
-
-protected theorem le_sup_right (f g : α →ₘ[μ] β) : g ≤ f ⊔ g := by
-  rw [← coeFn_le]
-  filter_upwards [coeFn_sup f g] with _ ha
-  rw [ha]
-  exact le_sup_right
-
-protected theorem sup_le (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f' := by
-  rw [← coeFn_le] at hf hg ⊢
-  filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup
-  rw [ha_sup]
-  exact sup_le haf hag
+instance instSemilatticeSup : SemilatticeSup (α →ₘ[μ] β) :=
+  toGerm_injective.semilatticeSup toGerm .rfl .rfl (comp₂_toGerm _ continuous_sup)
+
+protected theorem le_sup_left (f g : α →ₘ[μ] β) : f ≤ f ⊔ g :=
+  _root_.le_sup_left
+
+protected theorem le_sup_right (f g : α →ₘ[μ] β) : g ≤ f ⊔ g :=
+  _root_.le_sup_right
+
+protected theorem sup_le (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f' :=
+  _root_.sup_le hf hg
 
 end Sup
 
@@ -602,36 +596,21 @@ instance instInf : Min (α →ₘ[μ] β) where min f g := AEEqFun.comp₂ (· 
 theorem coeFn_inf (f g : α →ₘ[μ] β) : ⇑(f ⊓ g) =ᵐ[μ] fun x => f x ⊓ g x :=
   coeFn_comp₂ _ _ _ _
 
-protected theorem inf_le_left (f g : α →ₘ[μ] β) : f ⊓ g ≤ f := by
-  rw [← coeFn_le]
-  filter_upwards [coeFn_inf f g] with _ ha
-  rw [ha]
-  exact inf_le_left
+instance instSemilatticeInf : SemilatticeInf (α →ₘ[μ] β) :=
+  toGerm_injective.semilatticeInf toGerm .rfl .rfl (comp₂_toGerm _ continuous_inf)
+
+protected theorem inf_le_left (f g : α →ₘ[μ] β) : f ⊓ g ≤ f :=
+  _root_.inf_le_left
 
-protected theorem inf_le_right (f g : α →ₘ[μ] β) : f ⊓ g ≤ g := by
-  rw [← coeFn_le]
-  filter_upwards [coeFn_inf f g] with _ ha
-  rw [ha]
-  exact inf_le_right
+protected theorem inf_le_right (f g : α →ₘ[μ] β) : f ⊓ g ≤ g :=
+  _root_.inf_le_right
 
-protected theorem le_inf (f' f g : α →ₘ[μ] β) (hf : f' ≤ f) (hg : f' ≤ g) : f' ≤ f ⊓ g := by
-  rw [← coeFn_le] at hf hg ⊢
-  filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf
-  rw [ha_inf]
-  exact le_inf haf hag
+protected theorem le_inf (f' f g : α →ₘ[μ] β) (hf : f' ≤ f) (hg : f' ≤ g) : f' ≤ f ⊓ g :=
+  _root_.le_inf hf hg
 
 end Inf
 
-instance instLattice [Lattice β] [TopologicalLattice β] : Lattice (α →ₘ[μ] β) :=
-  { AEEqFun.instPartialOrder with
-    sup := max
-    le_sup_left := AEEqFun.le_sup_left
-    le_sup_right := AEEqFun.le_sup_right
-    sup_le := AEEqFun.sup_le
-    inf := min
-    inf_le_left := AEEqFun.inf_le_left
-    inf_le_right := AEEqFun.inf_le_right
-    le_inf := AEEqFun.le_inf }
+instance instLattice [Lattice β] [TopologicalLattice β] : Lattice (α →ₘ[μ] β) where
 
 end Lattice
 
diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
index 62d845f049e668..002ba891b4f87f 100644
--- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
+++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
@@ -357,27 +357,16 @@ theorem ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim (hm :
     exact hf_zero _ (hs.inter ht_meas) hμs
 
 theorem Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E} (hf : Integrable f μ)
-    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 := by
-  have hf_Lp : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
-  let f_Lp := hf_Lp.toLp f
-  have hf_f_Lp : f =ᵐ[μ] f_Lp := (MemLp.coeFn_toLp hf_Lp).symm
-  refine hf_f_Lp.trans ?_
-  refine Lp.ae_eq_zero_of_forall_setIntegral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top ?_ ?_
-  · exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _)
-  · intro s hs hμs
-    rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)]
-    exact hf_zero s hs hμs
+    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
+  hf.aefinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero
+    (fun _ _ _ => hf.integrableOn) hf_zero
 
 theorem Integrable.ae_eq_of_forall_setIntegral_eq (f g : α → E) (hf : Integrable f μ)
     (hg : Integrable g μ)
     (hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) :
-    f =ᵐ[μ] g := by
-  rw [← sub_ae_eq_zero]
-  have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
-    intro s hs hμs
-    rw [integral_sub' hf.integrableOn hg.integrableOn]
-    exact sub_eq_zero.mpr (hfg s hs hμs)
-  exact Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero (hf.sub hg) hfg'
+    f =ᵐ[μ] g :=
+  AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq (fun _ _ _ => hf.integrableOn)
+    (fun _ _ _ => hg.integrableOn) hfg hf.aefinStronglyMeasurable hg.aefinStronglyMeasurable
 
 variable {β : Type*} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]
 
diff --git a/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean b/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean
index 3cdb2645007327..8942c48fa04cd0 100644
--- a/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean
+++ b/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean
@@ -73,11 +73,7 @@ theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type
       _ = 0 := by simp only [tsum_zero]
   have ff' : ∀ᵐ x ∂μ, f x = f' x := by
     have : ∀ᵐ x ∂μ, x ∉ t := by
-      have : μ t = 0 := le_antisymm μt bot_le
-      change μ _ = 0
-      convert this
-      ext y
-      simp only [mem_setOf_eq, mem_compl_iff, not_notMem]
+      exact measure_eq_zero_iff_ae_notMem.1 (le_antisymm μt bot_le)
     filter_upwards [this] with x hx
     apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
     · intro i
@@ -86,18 +82,13 @@ theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type
       · simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem]
       simp only [H, piecewise_eq_of_mem]
       contrapose! hx
-      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (i : β) (f x) ∩ s :=
-        dense_iff_inter_open.1 s_dense (Ioo i (f x)) isOpen_Ioo (nonempty_Ioo.2 hx)
-      have A : x ∈ v i r := (huv i r).2.2.2.1 rq
-      refine mem_iUnion.2 ⟨i, ?_⟩
-      refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
-      exact ⟨H, A⟩
+      obtain ⟨r, rs, xr, rq⟩ := s_dense.exists_between hx
+      exact mem_iUnion₂.2 ⟨i, ⟨⟨r, ⟨rs, xr⟩⟩, H, (huv i r).2.2.2.1 rq⟩⟩
     · intro q hq
-      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
-        dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
-      refine ⟨⟨r, rs⟩, ?_⟩
-      have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
-      simp only [A, rq, piecewise_eq_of_mem]
+      obtain ⟨r, rs, xr, rq⟩ := s_dense.exists_between hq
+      exact ⟨⟨r, rs⟩, by
+        simp only [show x ∈ u' r from mem_biInter fun i _ => (huv r i).2.2.1 xr, rq,
+          piecewise_eq_of_mem]⟩
   exact ⟨f', f'_meas, ff'⟩
 
 /-- If a function `f : α → ℝ≥0∞` is such that the level sets `{f < p}` and `{q < f}` have measurable
diff --git a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
index 72724264ce6ac6..93dc03e76b71ef 100644
--- a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
+++ b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
@@ -114,12 +114,8 @@ theorem aeSeq_n_eq_fun_n_ae [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
 
 theorem iSup [SupSet β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
     (hp : ∀ᵐ x ∂μ, p x fun n => f n x) : ⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n := by
-  simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]
-  have h_ss : aeSeqSet hf p ⊆ { a : α | ⨆ i : ι, aeSeq hf p i a = ⨆ i : ι, f i a } := by
-    intro x hx
-    congr
-    exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
-  exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)
+  filter_upwards [aeSeq_eq_fun_ae hf hp] with x hx
+  simp [iSup_apply, hx]
 
 theorem iInf [InfSet β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
     (hp : ∀ᵐ x ∂μ, p x fun n ↦ f n x) : ⨅ n, aeSeq hf p n =ᵐ[μ] ⨅ n, f n :=
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
index 49af52b180db3b..740c93f4035c95 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
@@ -134,14 +134,9 @@ theorem memLp_trim_of_mem_lpMeasSubgroup (hm : m ≤ m0) (f : Lp F p μ)
     MemLp (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas).choose p (μ.trim hm) := by
   have hf : AEStronglyMeasurable[m] f μ :=
     mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
-  let g := hf.choose
-  obtain ⟨hg, hfg⟩ := hf.choose_spec
-  change MemLp g p (μ.trim hm)
-  refine ⟨hg.aestronglyMeasurable, ?_⟩
-  have h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm f p μ := by
-    rw [eLpNorm_trim hm hg]
-    exact eLpNorm_congr_ae hfg.symm
-  rw [h_eLpNorm_fg]
+  change MemLp (hf.mk f) p (μ.trim hm)
+  refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
+  rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]
   exact Lp.eLpNorm_lt_top f
 
 /-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subgroup
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean
index ab78aa5446f67b..3f6653a77bae8e 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/RadonNikodym.lean
@@ -61,11 +61,8 @@ lemma toReal_rnDeriv_map [IsFiniteMeasure μ] (hμν : μ ≪ ν)
   have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
   refine ae_eq_condExp_of_forall_setIntegral_eq _ (by fun_prop) ?_ ?_ ?_
   · rintro _ ⟨t, _, rfl⟩ _
-    refine Integrable.integrableOn ?_
-    change Integrable ((fun x ↦ ((μ.map g).rnDeriv (ν.map g) x).toReal) ∘ g) ν
-    rw [← integrable_map_measure (f := g) (Measurable.aestronglyMeasurable (by fun_prop))
-      (by fun_prop)]
-    fun_prop
+    exact Integrable.integrableOn <|
+      (Measure.integrable_toReal_rnDeriv (μ := μ.map g) (ν := ν.map g)).comp_measurable hg
   · rintro _ ⟨t, ht, rfl⟩ _
     calc ∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
     _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
@@ -91,10 +88,10 @@ lemma rnDeriv_map [IsFiniteMeasure μ] (hμν : μ ≪ ν)
   have h_ne_top1 : ∀ᵐ x ∂ν, (μ.map g).rnDeriv (ν.map g) (g x) ≠ ∞ :=
     ae_of_ae_map hg.aemeasurable (Measure.rnDeriv_ne_top (μ.map g) (ν.map g))
   have h_ne_top2 : ∀ᵐ x ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞ := by
-    refine condLExp_ne_top ?_
-    simp [Measure.lintegral_rnDeriv hμν]
-  have h_condExp := toReal_condLExp (m𝓨.comap g) (f := μ.rnDeriv ν) (μ := ν) (by fun_prop) ?_
-  swap; · simp [Measure.lintegral_rnDeriv hμν]
+    simpa [Measure.lintegral_rnDeriv hμν] using
+      (condLExp_ne_top (P := ν) (mΩ := m𝓨.comap g) (f := μ.rnDeriv ν))
+  have h_condExp := toReal_condLExp (m𝓨.comap g) (f := μ.rnDeriv ν) (μ := ν) (by fun_prop)
+    (by simp [Measure.lintegral_rnDeriv hμν])
   filter_upwards [toReal_rnDeriv_map hμν hg, h_condExp, h_ne_top1, h_ne_top2]
     with x hx h_condExp h_ne_top1 h_ne_top2
   rwa [← h_condExp, ENNReal.toReal_eq_toReal_iff' h_ne_top1 h_ne_top2] at hx
@@ -126,10 +123,10 @@ lemma toReal_rnDeriv_map_ae_eq_trim [IsFiniteMeasure μ] (hμν : μ ≪ ν)
       ν[(fun a ↦ (μ.rnDeriv ν a).toReal) | m𝓨.comap g] := by
   rw [StronglyMeasurable.ae_eq_trim_iff]
   · exact toReal_rnDeriv_map hμν hg
-  · refine Measurable.stronglyMeasurable fun s hs ↦ ?_
-    refine ⟨(fun a ↦ ((μ.map g).rnDeriv (ν.map g) a).toReal) ⁻¹' s, hs.preimage (by fun_prop), ?_⟩
-    rw [← Set.preimage_comp]
-    rfl
+  · simpa [Function.comp] using
+      (((Measure.measurable_rnDeriv
+          (μ.map g) (ν.map g)).ennreal_toReal).stronglyMeasurable.comp_measurable
+        (measurable_iff_comap_le.mpr le_rfl))
   · fun_prop
 
 /-- The Radon-Nikodym derivative `∂(μ.trim hm)/∂(ν.trim hm)` of the trimmed measures
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
index 975db020f35a9a..ea92903abee83c 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne, Kexing Ying
 module
 
 public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
+import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
 public import Mathlib.MeasureTheory.Function.UniformIntegrable
 public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
 
@@ -55,8 +56,6 @@ theorem rnDeriv_ae_eq_condExp {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)]
     exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable
   · exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable.aestronglyMeasurable
 
--- TODO: the following couple of lemmas should be generalized and proved using Jensen's inequality
--- for the conditional expectation (not in mathlib yet) .
 theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f | m]) 1 μ ≤ eLpNorm f 1 μ := by
   by_cases hf : Integrable f μ
   swap; · rw [condExp_of_not_integrable hf, eLpNorm_zero]; exact zero_le _
@@ -64,52 +63,35 @@ theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f | m]) 1
   swap; · rw [condExp_of_not_le hm, eLpNorm_zero]; exact zero_le _
   by_cases hsig : SigmaFinite (μ.trim hm)
   swap; · rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]; exact zero_le _
-  calc
-    eLpNorm (μ[f | m]) 1 μ ≤ eLpNorm (μ[(|f|) | m]) 1 μ := by
-      refine eLpNorm_mono_ae ?_
-      filter_upwards [condExp_mono hf hf.abs
-        (ae_of_all μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
-        (condExp_neg ..).symm.le.trans (condExp_mono hf.neg hf.abs
-          (ae_of_all μ (fun x => neg_le_abs (f x) : ∀ x, -f x ≤ |f x|)))] with x hx₁ hx₂
-      exact abs_le_abs hx₁ hx₂
-    _ = eLpNorm f 1 μ := by
-      rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm,
-        ← ENNReal.toReal_eq_toReal_iff' (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne
-          (hasFiniteIntegral_iff_enorm.mp hf.2).ne,
-        ← integral_norm_eq_lintegral_enorm
-          (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
-        ← integral_norm_eq_lintegral_enorm hf.1]
-      simp_rw [Real.norm_eq_abs]
-      rw (config := { occs := .pos [2] }) [← integral_condExp hm]
-      refine integral_congr_ae ?_
-      have : 0 ≤ᵐ[μ] μ[(|f|) | m] := by
-        rw [← condExp_zero]
-        exact condExp_mono (integrable_zero _ _ _) hf.abs
-          (ae_of_all μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))
-      filter_upwards [this] with x hx
-      exact abs_eq_self.2 hx
+  have hleft : eLpNorm (μ[f | m]) 1 μ ≠ ∞ := by
+    simpa [eLpNorm_one_eq_lintegral_enorm] using
+      (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne
+  have hright : eLpNorm f 1 μ ≠ ∞ := by
+    simpa [eLpNorm_one_eq_lintegral_enorm] using (hasFiniteIntegral_iff_enorm.mp hf.2).ne
+  rw [← ENNReal.toReal_le_toReal hleft hright]
+  rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm,
+    ← integral_norm_eq_lintegral_enorm (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
+    ← integral_norm_eq_lintegral_enorm hf.1]
+  refine (integral_mono_ae integrable_condExp.norm integrable_condExp norm_condExp_le).trans_eq ?_
+  exact integral_condExp (μ := μ) (m := m) (m₀ := m0) (f := fun x ↦ ‖f x‖) hm
 
 theorem integral_abs_condExp_le (f : α → ℝ) : ∫ x, |(μ[f | m]) x| ∂μ ≤ ∫ x, |f x| ∂μ := by
   by_cases hm : m ≤ m0
   swap
   · simp_rw [condExp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]
     positivity
+  by_cases hsig : SigmaFinite (μ.trim hm)
+  swap
+  · simp_rw [condExp_of_not_sigmaFinite hm hsig, Pi.zero_apply, abs_zero, integral_zero]
+    positivity
   by_cases hfint : Integrable f μ
   swap
   · simp only [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero, integral_const,
       smul_eq_mul, mul_zero]
     positivity
-  rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-  · apply ENNReal.toReal_mono <;> simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_enorm]
-    · exact hfint.2.ne
-    · rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm]
-      exact eLpNorm_one_condExp_le_eLpNorm _
-  · filter_upwards with x using abs_nonneg _
-  · simp_rw [← Real.norm_eq_abs]
-    exact hfint.1.norm
-  · filter_upwards with x using abs_nonneg _
-  · simp_rw [← Real.norm_eq_abs]
-    exact (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable.norm
+  simp_rw [← Real.norm_eq_abs]
+  refine (integral_mono_ae integrable_condExp.norm integrable_condExp norm_condExp_le).trans_eq ?_
+  exact integral_condExp (μ := μ) (m := m) (m₀ := m0) (f := fun x ↦ ‖f x‖) hm
 
 theorem setIntegral_abs_condExp_le {s : Set α} (hs : MeasurableSet[m] s) (f : α → ℝ) :
     ∫ x in s, |(μ[f | m]) x| ∂μ ≤ ∫ x in s, |f x| ∂μ := by
@@ -143,31 +125,21 @@ theorem ae_bdd_condExp_of_ae_bdd {R : ℝ≥0} {f : α → ℝ} (hbdd : ∀ᵐ x
   swap
   · simp_rw [condExp_of_not_le hnm, Pi.zero_apply, abs_zero]
     exact Eventually.of_forall fun _ => R.coe_nonneg
+  by_cases hsig : SigmaFinite (μ.trim hnm)
+  swap
+  · simp_rw [condExp_of_not_sigmaFinite hnm hsig, Pi.zero_apply, abs_zero]
+    exact Eventually.of_forall fun _ => R.coe_nonneg
   by_cases hfint : Integrable f μ
   swap
-  · simp_rw [condExp_of_not_integrable hfint]
+  · simp_rw [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero]
+    exact Eventually.of_forall fun _ => R.coe_nonneg
+  have hmem : ∀ᵐ x ∂μ, f x ∈ Set.Icc (-(R : ℝ)) R := by
     filter_upwards [hbdd] with x hx
-    rw [Pi.zero_apply, abs_zero]
-    exact (abs_nonneg _).trans hx
-  by_contra h
-  change μ _ ≠ 0 at h
-  simp only [← pos_iff_ne_zero, Set.compl_def, Set.mem_setOf_eq, not_le] at h
-  suffices μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R < μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R by
-    exact this.ne rfl
-  refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_
-  · exact integrable_condExp.abs.integrableOn
-  refine (setIntegral_abs_condExp_le ?_ _).trans ?_
-  · simp_rw [← Real.norm_eq_abs]
-    exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
-      stronglyMeasurable_condExp.norm.measurable
-  simp only [← smul_eq_mul, ← setIntegral_const]
-  refine setIntegral_mono_ae hfint.abs.integrableOn ?_ hbdd
-  refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_
-    (integrable_condExp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩
-  refine setLIntegral_mono
-    (stronglyMeasurable_condExp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => ?_
-  rw [enorm_eq_nnnorm, enorm_eq_nnnorm, ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg]
-  exact Subtype.mk_le_mk.2 (le_of_lt hx)
+    exact abs_le.mp hx
+  refine (Convex.condExp_mem (m := m) (mα := m0) hnm hfint isClosed_Icc
+    (convex_Icc _ _) hmem).mono ?_
+  intro x hx
+  exact abs_le.mpr hx
 
 /-- Given an integrable function `g`, the conditional expectations of `g` with respect to
 a sequence of sub-σ-algebras is uniformly integrable. -/
diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
index 3995e5cbafa6f1..4f5785dc127618 100644
--- a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
+++ b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
@@ -119,15 +119,11 @@ theorem exists_continuous_eLpNorm_sub_le_of_closed [μ.OuterRegular] (hp : p ≠
     refine Function.support_subset_iff'.2 fun x hx => ?_
     simp only [hgv hx, Pi.zero_apply, zero_smul]
   have gc_mem : MemLp (fun x => g x • c) p μ := by
-    refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)
-    refine ⟨g.continuous.aestronglyMeasurable, ?_⟩
-    have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
-      (eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.ne]
-    refine (eLpNorm_mono fun x => ?_).trans_lt this
-    by_cases hx : x ∈ v
-    · simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
-        indicator_of_mem, CStarRing.norm_one]
-    · simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]
+    have h_top : MemLp (fun x : α => g x • c) ∞ μ :=
+      memLp_top_of_bound (g.continuous.aestronglyMeasurable.smul_const c) ‖c‖
+        (Filter.Eventually.of_forall gc_bd0)
+    exact h_top.mono_exponent_of_measure_support_ne_top (s := v) (fun x hx => by simp [hgv hx])
+      hμv.ne le_top
   refine ⟨fun x ↦ g x • c, by fun_prop, (eLpNorm_mono gc_bd).trans ?_, gc_bd0,
       gc_support.trans inter_subset_left, gc_mem⟩
   exact hη _ ((measure_mono (diff_subset_diff inter_subset_right Subset.rfl)).trans hV.le)
diff --git a/Mathlib/MeasureTheory/Function/Egorov.lean b/Mathlib/MeasureTheory/Function/Egorov.lean
index f61bda8ec5123d..8b5c98729623d6 100644
--- a/Mathlib/MeasureTheory/Function/Egorov.lean
+++ b/Mathlib/MeasureTheory/Function/Egorov.lean
@@ -168,14 +168,9 @@ theorem tendstoUniformlyOn_diff_iUnionNotConvergentSeq (hε : 0 < ε)
   obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'
   rw [eventually_atTop]
   refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩
-  simp only [Set.mem_diff, Egorov.iUnionNotConvergentSeq, not_exists, Set.mem_iUnion,
-    Set.mem_inter_iff, not_and, exists_and_left] at hx
-  obtain ⟨hxs, hx⟩ := hx
-  specialize hx hxs N
-  rw [Egorov.mem_notConvergentSeq_iff] at hx
-  push Not at hx
-  rw [edist_comm]
-  exact lt_of_le_of_lt (hx n hn) hN
+  refine lt_of_le_of_lt ?_ hN
+  simpa [edist_comm] using not_lt.mp (show ¬ (N : ℝ≥0∞)⁻¹ < edist (f n x) (g x) from
+    fun h ↦ hx.2 <| Set.mem_iUnion.2 ⟨N, hx.1, Egorov.mem_notConvergentSeq_iff.2 ⟨n, hn, h⟩⟩)
 
 end Egorov
 
diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean
index da2c62782fd65b..bb5ca4cd919509 100644
--- a/Mathlib/MeasureTheory/Function/L2Space.lean
+++ b/Mathlib/MeasureTheory/Function/L2Space.lean
@@ -204,29 +204,11 @@ variable (𝕜) {s t : Set α}
 equal to the integral of the inner product over `s`: `∫ x in s, ⟪c, f x⟫ ∂μ`. -/
 theorem inner_indicatorConstLp_eq_setIntegral_inner (f : Lp E 2 μ) (hs : MeasurableSet s) (c : E)
     (hμs : μ s ≠ ∞) : (⟪indicatorConstLp 2 hs hμs c, f⟫ : 𝕜) = ∫ x in s, ⟪c, f x⟫ ∂μ := by
-  rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)]
-  have h_left : (∫ x in s, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = ∫ x in s, ⟪c, f x⟫ ∂μ := by
-    suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫ from
-      setIntegral_congr_ae hs h_ae_eq
-    have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c :=
-      indicatorConstLp_coeFn_mem
-    refine h_indicator.mono fun x hx hxs => ?_
-    congr
-    exact hx hxs
-  have h_right : (∫ x in sᶜ, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = 0 := by
-    suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0 by
-      simp_rw [← Set.mem_compl_iff] at h_ae_eq
-      suffices h_int_zero :
-          (∫ x in sᶜ, ⟪indicatorConstLp 2 hs hμs c x, f x⟫ ∂μ) = ∫ _ in sᶜ, 0 ∂μ by
-        rw [h_int_zero]
-        simp
-      exact setIntegral_congr_ae hs.compl h_ae_eq
-    have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 :=
-      indicatorConstLp_coeFn_notMem
-    refine h_indicator.mono fun x hx hxs => ?_
-    rw [hx hxs]
-    exact inner_zero_left _
-  rw [h_left, h_right, add_zero]
+  rw [inner_def, ← integral_indicator hs]
+  refine integral_congr_ae ((@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs c).mono fun x hx => ?_)
+  change ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = s.indicator (fun x => ⟪c, f x⟫) x
+  rw [hx]
+  by_cases hxs : x ∈ s <;> simp [hxs]
 
 /-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
 equal to the inner product of the constant `c` and the integral of `f` over `s`. -/
diff --git a/Mathlib/MeasureTheory/Function/LpOrder.lean b/Mathlib/MeasureTheory/Function/LpOrder.lean
index 5212b7ef885ea0..f696b44e0588f0 100644
--- a/Mathlib/MeasureTheory/Function/LpOrder.lean
+++ b/Mathlib/MeasureTheory/Function/LpOrder.lean
@@ -49,10 +49,7 @@ theorem coeFn_le (f g : Lp E p μ) : f ≤ᵐ[μ] g ↔ f ≤ g := by
 
 theorem coeFn_nonneg (f : Lp E p μ) : 0 ≤ᵐ[μ] f ↔ 0 ≤ f := by
   rw [← coeFn_le]
-  have h0 := Lp.coeFn_zero E p μ
-  constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2
-  · rwa [h2]
-  · rwa [← h2]
+  exact ⟨(Lp.coeFn_zero E p μ).trans_le, (Lp.coeFn_zero E p μ).symm.trans_le⟩
 
 variable [IsOrderedAddMonoid E]
 
@@ -113,13 +110,11 @@ theorem coeFn_abs (f : Lp E p μ) : ⇑|f| =ᵐ[μ] fun x => |f x| :=
 
 instance instHasSolidNorm [Fact (1 ≤ p)] :
     HasSolidNorm (Lp E p μ) :=
-  { solid := fun f g hfg => by
-      rw [← coeFn_le] at hfg
-      simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top f) (Lp.eLpNorm_ne_top g)]
-      refine eLpNorm_mono_ae ?_
-      filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg
-      rw [hxf, hxg] at hx
-      exact HasSolidNorm.solid hx }
+  ⟨fun f g hfg => by
+    simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top f) (Lp.eLpNorm_ne_top g)]
+    exact eLpNorm_mono_ae <|
+      (((Lp.coeFn_abs f).symm.trans_le ((coeFn_le (|f|) (|g|)).2 hfg)).trans_eq
+        (Lp.coeFn_abs g)).mono fun _ hx => norm_le_norm_of_abs_le_abs hx⟩
 
 end Lattice
 
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index e0a122dd1bc6d0..264378743af347 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -278,12 +278,8 @@ lemma eLpNorm'_mono_enorm_ae {f : α → ε} {g : α → ε'} (hq : 0 ≤ q) (h
   gcongr
 
 lemma eLpNorm'_mono_nnnorm_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
-    eLpNorm' f q μ ≤ eLpNorm' g q μ := by
-  simp only [eLpNorm'_eq_lintegral_enorm]
-  gcongr ?_ ^ (1 / q)
-  refine lintegral_mono_ae (h.mono fun x hx => ?_)
-  dsimp [enorm]
-  gcongr
+    eLpNorm' f q μ ≤ eLpNorm' g q μ :=
+  eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx
 
 theorem eLpNorm'_mono_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) :
     eLpNorm' f q μ ≤ eLpNorm' g q μ :=
@@ -327,12 +323,8 @@ theorem eLpNorm_mono_enorm_ae {f : α → ε} {g : α → ε'} (h : ∀ᵐ x ∂
   · exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h
 
 theorem eLpNorm_mono_nnnorm_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
-    eLpNorm f p μ ≤ eLpNorm g p μ := by
-  simp only [eLpNorm]
-  split_ifs
-  · exact le_rfl
-  · exact essSup_mono_ae (h.mono fun x hx => ENNReal.coe_le_coe.mpr hx)
-  · exact eLpNorm'_mono_nnnorm_ae ENNReal.toReal_nonneg h
+    eLpNorm f p μ ≤ eLpNorm g p μ :=
+  eLpNorm_mono_enorm_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx
 
 theorem eLpNorm_mono_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) :
     eLpNorm f p μ ≤ eLpNorm g p μ :=
@@ -401,13 +393,9 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM
 
 theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
     eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by
-  rcases eq_zero_or_neZero μ with rfl | hμ
-  · simp
-  by_cases hp : p = 0
-  · simp [hp]
-  have : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖(C : ℝ)‖₊ := hfC.mono fun x hx => hx.trans_eq C.nnnorm_eq.symm
-  refine (eLpNorm_mono_ae this).trans_eq ?_
-  rw [eLpNorm_const _ hp (NeZero.ne μ), C.enorm_eq, one_div, ENNReal.smul_def, smul_eq_mul]
+  simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using
+    (eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞))
+      (hfC.mono fun _ hx => by simpa using hx))
 
 theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
     eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
index 57377f7cec7370..6b18736ed9916d 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
@@ -34,22 +34,17 @@ lemma enorm_le_eLpNorm_count (f : α → ε) (i : α) (hp : p ≠ 0) :
       _ = eLpNorm f p (count.restrict {i}) := by simp
       _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..
 
+omit [MeasurableSingletonClass α] in
 lemma eLpNorm_count_lt_top_of_lt [Finite α] (h : ∀ i, ‖f i‖ₑ < ∞) :
     eLpNorm f p .count < ∞ := by
   letI _ := Fintype.ofFinite α
-  simp_rw [eLpNorm]
-  split_ifs with h2 h3
-  · exact ENNReal.zero_lt_top
-  · refine (essSup_le_of_ae_le (Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_
-    · filter_upwards with x
-      exact Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ _)
-    · simp_rw [Finset.sup_lt_iff ENNReal.zero_lt_top, h, implies_true]
-  · refine (ENNReal.rpow_lt_top_iff_of_pos ?_).mpr ?_
-    · rw [one_div, inv_pos]
-      exact ENNReal.toReal_pos h2 h3
-    · simp_rw [lintegral_count, tsum_eq_sum (s := Finset.univ) (by simp), ENNReal.sum_lt_top,
-        Finset.mem_univ, forall_const, ENNReal.rpow_lt_top_iff_of_pos (ENNReal.toReal_pos h2 h3), h,
-        implies_true]
+  let C : ℝ≥0∞ := Finset.univ.sup (‖f ·‖ₑ)
+  have hC : ∀ x, ‖f x‖ₑ ≤ C := fun x => Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)
+  have hC_lt : C < ∞ := by
+    simp [C, Finset.sup_lt_iff, h]
+  refine (eLpNorm_mono_enorm (μ := (count : Measure α)) (p := p) (f := f)
+    (g := fun _ : α => C) fun x => by simpa [C] using hC x).trans_lt ?_
+  exact (memLp_const_enorm (μ := (count : Measure α)) (p := p) (c := C) hC_lt.ne).eLpNorm_lt_top
 
 lemma eLpNorm_count_lt_top [Finite α] (hp : p ≠ 0) :
     eLpNorm f p .count < ∞ ↔ ∀ i, ‖f i‖ₑ < ∞ :=
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
index f98a3bca0bb08f..e525926a3adac2 100644
--- a/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
+++ b/Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
@@ -141,22 +141,15 @@ theorem MemLp.sub {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : Mem
   rw [sub_eq_add_neg]
   exact hf.add hg.neg
 
-theorem memLp_finset_sum [ContinuousAdd ε']
+theorem memLp_finset_sum' [ContinuousAdd ε']
     {ι} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
-    MemLp (fun a => ∑ i ∈ s, f i a) p μ := by
-  haveI : DecidableEq ι := Classical.decEq _
-  revert hf
-  refine Finset.induction_on s ?_ ?_
-  · simp only [MemLp.zero', Finset.sum_empty, imp_true_iff]
-  · intro i s his ih hf
-    simp only [his, Finset.sum_insert, not_false_iff]
-    exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))
+    MemLp (∑ i ∈ s, f i) p μ :=
+  Finset.sum_induction f (fun g => MemLp g p μ) (fun _ _ => MemLp.add)
+    (MemLp.zero' (μ := μ) (p := p)) hf
 
-theorem memLp_finset_sum' [ContinuousAdd ε']
+theorem memLp_finset_sum [ContinuousAdd ε']
     {ι} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
-    MemLp (∑ i ∈ s, f i) p μ := by
-  convert memLp_finset_sum s hf using 1
-  ext x
-  simp
+    MemLp (fun a => ∑ i ∈ s, f i a) p μ := by
+  simpa only [← Finset.sum_apply] using memLp_finset_sum' (μ := μ) (p := p) s hf
 
 end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean b/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
index 155d4adbf97dc9..2aaed0da3f3107 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
@@ -676,12 +676,8 @@ theorem memLp_comp_iff_of_antilipschitz {α E F} {K K'} [MeasurableSpace α] {μ
 defined as an element of `Lp`. -/
 def compLp (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) : Lp F p μ :=
   ⟨AEEqFun.comp g hg.continuous (f : α →ₘ[μ] E), by
-    suffices ∀ᵐ x ∂μ, ‖AEEqFun.comp g hg.continuous (f : α →ₘ[μ] E) x‖ ≤ c * ‖f x‖ from
-      Lp.mem_Lp_of_ae_le_mul this
-    filter_upwards [AEEqFun.coeFn_comp g hg.continuous (f : α →ₘ[μ] E)] with a ha
-    simp only [ha]
-    rw [← dist_zero_right, ← dist_zero_right, ← g0]
-    exact hg.dist_le_mul (f a) 0⟩
+    rw [Lp.mem_Lp_iff_memLp]
+    exact (hg.comp_memLp g0 (Lp.memLp f)).ae_eq (AEEqFun.coeFn_comp _ hg.continuous _).symm⟩
 
 theorem coeFn_compLp (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) :
     hg.compLp g0 f =ᵐ[μ] g ∘ f :=
diff --git a/Mathlib/MeasureTheory/Function/LpSpace/Complete.lean b/Mathlib/MeasureTheory/Function/LpSpace/Complete.lean
index 8f6b245b010ec6..6c3390f62a659a 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace/Complete.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace/Complete.lean
@@ -282,26 +282,14 @@ theorem ae_tendsto_of_cauchy_eLpNorm' [CompleteSpace E] {f : ℕ → α → E} {
     have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
       tsum_enorm_sub_ae_lt_top hf hp1 hB h3
     exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne
-  have h :
-    ∀ᵐ x ∂μ, ∃ l : E,
-      atTop.Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) (𝓝 l) := by
-    refine h_summable.mono fun x hx => ?_
-    let hx_sum := hx.hasSum.tendsto_sum_nat
-    exact ⟨∑' i, (f (i + 1) x - f i x), hx_sum⟩
-  refine h.mono fun x hx => ?_
-  obtain ⟨l, hx⟩ := hx
-  have h_rw_sum :
-      (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x := by
-    ext1 n
-    change
-      (∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i)) = f n x - f 0 x
-    rw [Finset.sum_range_sub (fun m => f m x)]
-  rw [h_rw_sum] at hx
-  have hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x := by
-    ext1 n
-    abel
-  rw [hf_rw]
-  exact ⟨l + f 0 x, Tendsto.add_const _ hx⟩
+  refine h_summable.mono fun x hx => ?_
+  have hsum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x := by
+    ext n
+    exact Finset.sum_range_sub (fun m => f m x) n
+  have hx_sum := hx.hasSum.tendsto_sum_nat
+  rw [hsum] at hx_sum
+  refine ⟨∑' i, (f (i + 1) x - f i x) + f 0 x, ?_⟩
+  simpa [sub_eq_add_neg, add_assoc] using hx_sum.add_const (f 0 x)
 
 theorem ae_tendsto_of_cauchy_eLpNorm [CompleteSpace E] {f : ℕ → α → E}
     (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hp : 1 ≤ p) {B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞)
@@ -341,21 +329,13 @@ theorem cauchy_tendsto_of_tendsto {f : ℕ → α → E} (hf : ∀ n, AEStrongly
     atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) := by
   rw [ENNReal.tendsto_atTop_zero]
   intro ε hε
-  have h_B : ∃ N : ℕ, B N ≤ ε := by
-    suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
-      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
-    exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
-  obtain ⟨N, h_B⟩ := h_B
+  obtain ⟨N, h_B⟩ :=
+    ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB) ε hε
   refine ⟨N, fun n hn => ?_⟩
-  have h_sub : eLpNorm (f n - f_lim) p μ ≤ atTop.liminf fun m => eLpNorm (f n - f m) p μ := by
-    refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_
-    refine h_lim.mono fun x hx => ?_
-    simp_rw [sub_eq_add_neg]
-    exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)
-  refine h_sub.trans ?_
-  refine liminf_le_of_frequently_le' (frequently_atTop.mpr ?_)
-  refine fun N1 => ⟨max N N1, le_max_right _ _, ?_⟩
-  exact (h_cau N n (max N N1) hn (le_max_left _ _)).le.trans h_B
+  refine (eLpNorm_le_of_ae_tendsto
+    ((Filter.eventually_ge_atTop N).mono fun m hm => (h_cau N n m hn hm).le)
+    (fun m => (hf n).sub (hf m)) ?_).trans (h_B N le_rfl)
+  exact h_lim.mono fun x hx => tendsto_const_nhds.sub hx
 
 theorem memLp_of_cauchy_tendsto (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ n, MemLp (f n) p μ)
     (f_lim : α → E) (h_lim_meas : AEStronglyMeasurable f_lim μ)
diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean
index 91bbff2ab208d1..6786252a3f4191 100644
--- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean
+++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean
@@ -1328,24 +1328,7 @@ theorem _root_.Measurable.add_simpleFunc
     {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E]
     {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) :
     Measurable (g + (f : α → E)) := by
-  classical
-  induction f using SimpleFunc.induction with
-  | @const c s hs =>
-    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
-      SimpleFunc.coe_zero]
-    rw [← s.piecewise_same g, ← piecewise_add]
-    exact Measurable.piecewise hs (hg.add_const _) (hg.add_const _)
-  | @add f f' hff' hf hf' =>
-    have : (g + ↑(f + f')) = (Function.support f).piecewise (g + (f : α → E)) (g + f') := by
-      ext x
-      by_cases hx : x ∈ Function.support f
-      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
-          Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_right_inj, add_eq_left]
-          using Set.disjoint_left.1 hff' hx
-      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
-          Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_right_inj, add_eq_right] using hx
-    rw [this]
-    exact Measurable.piecewise f.measurableSet_support hf hf'
+  simpa using f.measurable_bind (fun b a => g a + b) fun b => hg.add_const b
 
 /-- In a topological vector space, the addition of a simple function and a measurable function is
 measurable. -/
@@ -1353,24 +1336,7 @@ theorem _root_.Measurable.simpleFunc_add
     {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E]
     {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) :
     Measurable ((f : α → E) + g) := by
-  classical
-  induction f using SimpleFunc.induction with
-  | @const c s hs =>
-    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
-      SimpleFunc.coe_zero]
-    rw [← s.piecewise_same g, ← piecewise_add]
-    exact Measurable.piecewise hs (hg.const_add _) (hg.const_add _)
-  | @add f f' hff' hf hf' =>
-    have : (↑(f + f') + g) = (Function.support f).piecewise ((f : α → E) + g) (f' + g) := by
-      ext x
-      by_cases hx : x ∈ Function.support f
-      · simpa only [coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
-          Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_left_inj, add_eq_left]
-          using Set.disjoint_left.1 hff' hx
-      · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not,
-          Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_left_inj, add_eq_right] using hx
-    rw [this]
-    exact Measurable.piecewise f.measurableSet_support hf hf'
+  simpa using f.measurable_bind (fun b a => b + g a) fun b => hg.const_add b
 
 end SimpleFunc
 
diff --git a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
index 96154ab2995296..dd6163309ae704 100644
--- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
+++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
@@ -271,26 +271,18 @@ protected theorem eLpNorm'_eq {p : ℝ} (f : α →ₛ F) (μ : Measure α) :
 theorem measure_preimage_lt_top_of_memLp (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) (f : α →ₛ E)
     (hf : MemLp f p μ) (y : E) (hy_ne : y ≠ 0) : μ (f ⁻¹' {y}) < ∞ := by
   have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top
-  have hf_eLpNorm := MemLp.eLpNorm_lt_top hf
-  rw [eLpNorm_eq_eLpNorm' hp_pos hp_ne_top, f.eLpNorm'_eq, one_div,
-    ← @ENNReal.lt_rpow_inv_iff _ _ p.toReal⁻¹ (by simp [hp_pos_real]),
-    @ENNReal.top_rpow_of_pos p.toReal⁻¹⁻¹ (by simp [hp_pos_real]),
-    ENNReal.sum_lt_top] at hf_eLpNorm
-  by_cases hyf : y ∈ f.range
-  swap
-  · suffices h_empty : f ⁻¹' {y} = ∅ by
-      rw [h_empty, measure_empty]; exact ENNReal.coe_lt_top
-    exact (preimage_eq_empty_iff _ _).mpr hyf
-  specialize hf_eLpNorm y hyf
-  rw [ENNReal.mul_lt_top_iff] at hf_eLpNorm
-  cases hf_eLpNorm with
-  | inl hf_eLpNorm => exact hf_eLpNorm.2
-  | inr hf_eLpNorm =>
-    cases hf_eLpNorm with
-    | inl hf_eLpNorm =>
-      refine absurd ?_ hy_ne
-      simpa [hp_pos_real] using hf_eLpNorm
-    | inr hf_eLpNorm => simp [hf_eLpNorm]
+  have h_lin :
+      (f.map fun x => ‖x‖ₑ ^ p.toReal).lintegral μ = ∫⁻ a, ‖f a‖ₑ ^ p.toReal ∂μ := by
+    simpa using ((f.map fun x => ‖x‖ₑ ^ p.toReal).lintegral_eq_lintegral μ).symm
+  have h_fin : (f.map fun x => ‖x‖ₑ ^ p.toReal).FinMeasSupp μ := by
+    refine SimpleFunc.FinMeasSupp.of_lintegral_ne_top ?_
+    rw [h_lin]
+    exact (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_pos hp_ne_top hf.eLpNorm_lt_top).ne
+  have hf_fin : f.FinMeasSupp μ := by
+    rwa [SimpleFunc.FinMeasSupp.map_iff (g := fun x => ‖x‖ₑ ^ p.toReal) (by
+      intro x
+      simp [ENNReal.rpow_eq_zero_iff_of_pos hp_pos_real, enorm_eq_zero])] at h_fin
+  exact hf_fin.meas_preimage_singleton_ne_zero hy_ne
 
 theorem memLp_of_finite_measure_preimage (p : ℝ≥0∞) {f : α →ₛ E}
     (hf : ∀ y, y ≠ 0 → μ (f ⁻¹' {y}) < ∞) : MemLp f p μ := by
@@ -548,40 +540,33 @@ theorem toSimpleFunc_toLp (f : α →ₛ E) (hfi : MemLp f p μ) : toSimpleFunc
 variable (E μ)
 
 theorem zero_toSimpleFunc : toSimpleFunc (0 : Lp.simpleFunc E p μ) =ᵐ[μ] 0 := by
-  filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ),
-    Lp.coeFn_zero E 1 μ] with _ h₁ _
-  rwa [h₁]
+  exact (toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ)).trans <| Lp.coeFn_zero E 1 μ
 
 variable {E μ}
 
 theorem add_toSimpleFunc (f g : Lp.simpleFunc E p μ) :
     toSimpleFunc (f + g) =ᵐ[μ] toSimpleFunc f + toSimpleFunc g := by
-  filter_upwards [toSimpleFunc_eq_toFun (f + g), toSimpleFunc_eq_toFun f,
-    toSimpleFunc_eq_toFun g, Lp.coeFn_add (f : Lp E p μ) g] with _
-  simp only [AddSubgroup.coe_add, Pi.add_apply]
-  iterate 4 intro h; rw [h]
+  refine (toSimpleFunc_eq_toFun (f + g)).trans ?_
+  refine (Lp.coeFn_add (f : Lp E p μ) g).trans ?_
+  exact (toSimpleFunc_eq_toFun f).symm.add (toSimpleFunc_eq_toFun g).symm
 
 theorem neg_toSimpleFunc (f : Lp.simpleFunc E p μ) : toSimpleFunc (-f) =ᵐ[μ] -toSimpleFunc f := by
-  filter_upwards [toSimpleFunc_eq_toFun (-f), toSimpleFunc_eq_toFun f,
-    Lp.coeFn_neg (f : Lp E p μ)] with _
-  simp only [Pi.neg_apply, AddSubgroup.coe_neg]
-  repeat intro h; rw [h]
+  refine (toSimpleFunc_eq_toFun (-f)).trans ?_
+  exact (Lp.coeFn_neg (f : Lp E p μ)).trans (toSimpleFunc_eq_toFun f).symm.neg
 
 theorem sub_toSimpleFunc (f g : Lp.simpleFunc E p μ) :
     toSimpleFunc (f - g) =ᵐ[μ] toSimpleFunc f - toSimpleFunc g := by
-  filter_upwards [toSimpleFunc_eq_toFun (f - g), toSimpleFunc_eq_toFun f,
-    toSimpleFunc_eq_toFun g, Lp.coeFn_sub (f : Lp E p μ) g] with _
-  simp only [AddSubgroup.coe_sub, Pi.sub_apply]
-  repeat' intro h; rw [h]
+  refine (toSimpleFunc_eq_toFun (f - g)).trans ?_
+  refine (Lp.coeFn_sub (f : Lp E p μ) g).trans ?_
+  exact (toSimpleFunc_eq_toFun f).symm.sub (toSimpleFunc_eq_toFun g).symm
 
 variable [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E]
 
 theorem smul_toSimpleFunc (k : 𝕜) (f : Lp.simpleFunc E p μ) :
     toSimpleFunc (k • f) =ᵐ[μ] k • ⇑(toSimpleFunc f) := by
-  filter_upwards [toSimpleFunc_eq_toFun (k • f), toSimpleFunc_eq_toFun f,
-    Lp.coeFn_smul k (f : Lp E p μ)] with _
-  simp only [Pi.smul_apply, coe_smul]
-  repeat intro h; rw [h]
+  refine (toSimpleFunc_eq_toFun (k • f)).trans ?_
+  exact (Lp.coeFn_smul k (f : Lp E p μ)).trans <|
+    EventuallyEq.const_smul (toSimpleFunc_eq_toFun f).symm k
 
 theorem norm_toSimpleFunc [Fact (1 ≤ p)] (f : Lp.simpleFunc E p μ) :
     ‖f‖ = ENNReal.toReal (eLpNorm (toSimpleFunc f) p μ) := by
diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
index f9d61c0de973f8..b1612cbac1c575 100644
--- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
@@ -977,19 +977,13 @@ theorem stronglyMeasurable_in_set {m : MeasurableSpace α} [TopologicalSpace β]
     (hf_zero : ∀ x, x ∉ s → f x = 0) :
     ∃ fs : ℕ → α →ₛ β,
       (∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ n, fs n x = 0 := by
-  let g_seq_s : ℕ → @SimpleFunc α m β := fun n => (hf.approx n).restrict s
-  have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x := by
-    intro x hx n
-    rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
-  have hg_zero : ∀ x ∉ s, ∀ n, g_seq_s n x = 0 := by
-    intro x hx n
-    rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]
-  refine ⟨g_seq_s, fun x => ?_, hg_zero⟩
-  by_cases hx : x ∈ s
-  · simp_rw [hg_eq x hx]
-    exact hf.tendsto_approx x
-  · simp_rw [hg_zero x hx, hf_zero x hx]
-    exact tendsto_const_nhds
+  refine ⟨fun n => (hf.approx n).restrict s, ?_, ?_⟩
+  · intro x
+    by_cases hx : x ∈ s
+    · simpa [SimpleFunc.coe_restrict, hs, hx] using hf.tendsto_approx x
+    · simpa [SimpleFunc.coe_restrict, hs, hx, hf_zero x hx] using tendsto_const_nhds
+  · intro x hx n
+    simp [SimpleFunc.coe_restrict, hs, hx]
 
 /-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
 another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` supported
diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean
index 49333de91686c9..9a1e464c9ede56 100644
--- a/Mathlib/Probability/ProductMeasure.lean
+++ b/Mathlib/Probability/ProductMeasure.lean
@@ -89,7 +89,7 @@ theorem piContent_eq_measure_pi [Fintype ι] {s : Set (Π i, X i)} (hs : Measura
   have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl
   nth_rw 1 [this]
   dsimp [e]
-  rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e,
+  rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← MeasureTheory.pi_map_piCongrLeft e,
     ← Measure.map_apply (by fun_prop) hs]; rfl
 
 end Preliminaries