refactor: golf Function/SimpleFunc, Function/LpSeminorm, Constructions/Polish

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
 

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 ?_ ?_ ?_ ?_ ?_⟩

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)] :

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 β]

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 ℝ))⟩⟩

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

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, ?_, ?_, ?_, ?_, ?_⟩

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
 

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 β]
 

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

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 :=