[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
⊢ AEMeasurable f
[PROOFSTEP]
haveI : Encodable s := s_count.toEncodable
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
⊢ AEMeasurable f
[PROOFSTEP]
have h' :
  ∀ p q,
    ∃ u v,
      MeasurableSet u ∧
        MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0) :=
  by
  intro p q
  by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
  · rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
    exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
  · refine' ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _, fun ps qs pq => _⟩
    simp only [not_and] at H 
    exact (H ps qs pq).elim
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
⊢ ∀ (p q : β),
    ∃ u v,
      MeasurableSet u ∧
        MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
[PROOFSTEP]
intro p q
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
⊢ ∃ u v,
    MeasurableSet u ∧
      MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
[PROOFSTEP]
by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
[GOAL]
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
⊢ ∃ u v,
    MeasurableSet u ∧
      MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
[PROOFSTEP]
rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
[GOAL]
case pos.intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
h'u : {x | f x < p} ⊆ u
h'v : {x | q < f x} ⊆ v
hμ : ↑↑μ (u ∩ v) = 0
⊢ ∃ u v,
    MeasurableSet u ∧
      MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
[PROOFSTEP]
exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
[GOAL]
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
⊢ ∃ u v,
    MeasurableSet u ∧
      MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
[PROOFSTEP]
refine' ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _, fun ps qs pq => _⟩
[GOAL]
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
ps : p ∈ s
qs : q ∈ s
pq : p < q
⊢ ↑↑μ (univ ∩ univ) = 0
[PROOFSTEP]
simp only [not_and] at H 
[GOAL]
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
ps : p ∈ s
qs : q ∈ s
pq : p < q
H : p ∈ s → q ∈ s → ¬p < q
⊢ ↑↑μ (univ ∩ univ) = 0
[PROOFSTEP]
exact (H ps qs pq).elim
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
h' :
  ∀ (p q : β),
    ∃ u v,
      MeasurableSet u ∧
        MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u ∩ v) = 0)
⊢ AEMeasurable f
[PROOFSTEP]
choose! u v huv using h'
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
⊢ AEMeasurable f
[PROOFSTEP]
let u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
⊢ AEMeasurable f
[PROOFSTEP]
have u'_meas : ∀ i, MeasurableSet (u' i) := by
  intro i
  exact MeasurableSet.biInter (s_count.mono (inter_subset_left _ _)) fun b _ => (huv i b).1
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
⊢ ∀ (i : β), MeasurableSet (u' i)
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
i : β
⊢ MeasurableSet (u' i)
[PROOFSTEP]
exact MeasurableSet.biInter (s_count.mono (inter_subset_left _ _)) fun b _ => (huv i b).1
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
⊢ AEMeasurable f
[PROOFSTEP]
let f' : α → β := fun x => ⨅ i : s, piecewise (u' i) (fun _ => (i : β)) (fun _ => (⊤ : β)) x
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
⊢ AEMeasurable f
[PROOFSTEP]
have f'_meas : Measurable f' := by
  apply measurable_iInf
  exact fun i => Measurable.piecewise (u'_meas i) measurable_const measurable_const
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
⊢ Measurable f'
[PROOFSTEP]
apply measurable_iInf
[GOAL]
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
⊢ ∀ (i : ↑s), Measurable fun b => piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) b
[PROOFSTEP]
exact fun i => Measurable.piecewise (u'_meas i) measurable_const measurable_const
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
⊢ AEMeasurable f
[PROOFSTEP]
let t := ⋃ (p : s) (q : ↥(s ∩ Ioi p)), u' p ∩ v p q
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ AEMeasurable f
[PROOFSTEP]
have μt : μ t ≤ 0 :=
  calc
    μ t ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u' p ∩ v p q) :=
      by
      refine (measure_iUnion_le _).trans ?_
      refine ENNReal.tsum_le_tsum fun p => ?_
      refine @measure_iUnion_le _ _ _ _ ?_ _
      exact (s_count.mono (inter_subset_left _ _)).to_subtype
    _ ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u p q ∩ v p q) :=
      by
      refine ENNReal.tsum_le_tsum fun p => ?_
      refine ENNReal.tsum_le_tsum fun q => measure_mono ?_
      exact inter_subset_inter_left _ (biInter_subset_of_mem q.2)
    _ = ∑' (p : s) (_ : ↥(s ∩ Ioi p)), (0 : ℝ≥0∞) := by
      congr
      ext1 p
      congr
      ext1 q
      exact (huv p q).2.2.2.2 p.2 q.2.1 q.2.2
    _ = 0 := by simp only [tsum_zero]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ ↑↑μ t ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u' ↑p ∩ v ↑p ↑q)
[PROOFSTEP]
refine (measure_iUnion_le _).trans ?_
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ ∑' (i : ↑s), ↑↑μ (⋃ (q : ↑(s ∩ Ioi ↑i)), u' ↑i ∩ v ↑i ↑q) ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u' ↑p ∩ v ↑p ↑q)
[PROOFSTEP]
refine ENNReal.tsum_le_tsum fun p => ?_
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
⊢ ↑↑μ (⋃ (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q) ≤ ∑' (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u' ↑p ∩ v ↑p ↑q)
[PROOFSTEP]
refine @measure_iUnion_le _ _ _ _ ?_ _
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
⊢ Countable ↑(s ∩ Ioi ↑p)
[PROOFSTEP]
exact (s_count.mono (inter_subset_left _ _)).to_subtype
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u' ↑p ∩ v ↑p ↑q) ≤ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q)
[PROOFSTEP]
refine ENNReal.tsum_le_tsum fun p => ?_
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
⊢ ∑' (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u' ↑p ∩ v ↑p ↑q) ≤ ∑' (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q)
[PROOFSTEP]
refine ENNReal.tsum_le_tsum fun q => measure_mono ?_
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
q : ↑(s ∩ Ioi ↑p)
⊢ u' ↑p ∩ v ↑p ↑q ⊆ u ↑p ↑q ∩ v ↑p ↑q
[PROOFSTEP]
exact inter_subset_inter_left _ (biInter_subset_of_mem q.2)
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q) = ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ (fun p => ∑' (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q)) = fun p => ∑' (x : ↑(s ∩ Ioi ↑p)), 0
[PROOFSTEP]
ext1 p
[GOAL]
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
⊢ ∑' (q : ↑(s ∩ Ioi ↑p)), ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q) = ∑' (x : ↑(s ∩ Ioi ↑p)), 0
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_f
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
⊢ (fun q => ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q)) = fun x => 0
[PROOFSTEP]
ext1 q
[GOAL]
case e_f.h.e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
p : ↑s
q : ↑(s ∩ Ioi ↑p)
⊢ ↑↑μ (u ↑p ↑q ∩ v ↑p ↑q) = 0
[PROOFSTEP]
exact (huv p q).2.2.2.2 p.2 q.2.1 q.2.2
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0 = 0
[PROOFSTEP]
simp only [tsum_zero]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
⊢ AEMeasurable f
[PROOFSTEP]
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 [not_exists, exists_prop, mem_setOf_eq, mem_compl_iff, not_not_mem]
  filter_upwards [this] with x hx
  apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
  · intro i
    by_cases H : x ∈ u' i
    swap
    · simp only [H, le_top, not_false_iff, piecewise_eq_of_not_mem]
    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⟩
  · 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, Subtype.coe_mk]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
⊢ ∀ᵐ (x : α) ∂μ, f x = f' x
[PROOFSTEP]
have : ∀ᵐ x ∂μ, x ∉ t := by
  have : μ t = 0 := le_antisymm μt bot_le
  change μ _ = 0
  convert this
  ext y
  simp only [not_exists, exists_prop, mem_setOf_eq, mem_compl_iff, not_not_mem]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ t
[PROOFSTEP]
have : μ t = 0 := le_antisymm μt bot_le
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ↑↑μ t = 0
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ t
[PROOFSTEP]
change μ _ = 0
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ↑↑μ t = 0
⊢ ↑↑μ {x | (fun x => ¬x ∈ t) x}ᶜ = 0
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ↑↑μ t = 0
⊢ {x | (fun x => ¬x ∈ t) x}ᶜ = t
[PROOFSTEP]
ext y
[GOAL]
case h.e'_2.h.e'_3.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ↑↑μ t = 0
y : α
⊢ y ∈ {x | (fun x => ¬x ∈ t) x}ᶜ ↔ y ∈ t
[PROOFSTEP]
simp only [not_exists, exists_prop, mem_setOf_eq, mem_compl_iff, not_not_mem]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, f x = f' x
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
⊢ f x = ⨅ (i : ↑s), piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
⊢ ∀ (i : ↑s), f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
⊢ f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
by_cases H : x ∈ u' i
[GOAL]
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
H : x ∈ u' ↑i
⊢ f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
H : ¬x ∈ u' ↑i
⊢ f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
H : ¬x ∈ u' ↑i
⊢ f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
simp only [H, le_top, not_false_iff, piecewise_eq_of_not_mem]
[GOAL]
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
H : x ∈ u' ↑i
⊢ f x ≤ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x
[PROOFSTEP]
simp only [H, piecewise_eq_of_mem]
[GOAL]
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
i : ↑s
H : x ∈ u' ↑i
⊢ f x ≤ ↑i
[PROOFSTEP]
contrapose! hx
[GOAL]
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
⊢ x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
[PROOFSTEP]
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)
[GOAL]
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
⊢ x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
[PROOFSTEP]
have A : x ∈ v i r := (huv i r).2.2.2.1 rq
[GOAL]
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
[PROOFSTEP]
refine mem_iUnion.2 ⟨i, ?_⟩
[GOAL]
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ ⋃ (q : ↑(s ∩ Ioi ↑i)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) ∩ v ↑i ↑q
[PROOFSTEP]
refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
[GOAL]
case pos.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
i : ↑s
H : x ∈ u' ↑i
hx : ↑i < f x
r : β
rs : r ∈ s
xr : ↑i < r
rq : r < f x
A : x ∈ v (↑i) r
⊢ x ∈ (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) ∩ v ↑i ↑{ val := r, property := (_ : r ∈ s ∧ r ∈ Ioi ↑i) }
[PROOFSTEP]
exact ⟨H, A⟩
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
⊢ ∀ (w : β), f x < w → ∃ i, piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x < w
[PROOFSTEP]
intro q hq
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
q : β
hq : f x < q
⊢ ∃ i, piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x < q
[PROOFSTEP]
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)
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
⊢ ∃ i, piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑i), u (↑i) q) (fun x => ↑i) (fun x => ⊤) x < q
[PROOFSTEP]
refine' ⟨⟨r, rs⟩, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
⊢ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑{ val := r, property := rs }), u (↑{ val := r, property := rs }) q)
      (fun x => ↑{ val := r, property := rs }) (fun x => ⊤) x <
    q
[PROOFSTEP]
have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
x : α
hx : ¬x ∈ ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑p), u (↑p) q) ∩ v ↑p ↑q
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
A : x ∈ u' r
⊢ piecewise (⋂ (q : β) (_ : q ∈ s ∩ Ioi ↑{ val := r, property := rs }), u (↑{ val := r, property := rs }) q)
      (fun x => ↑{ val := r, property := rs }) (fun x => ⊤) x <
    q
[PROOFSTEP]
simp only [A, rq, piecewise_eq_of_mem, Subtype.coe_mk]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : Set.Countable s
s_dense : Dense s
f : α → β
h :
  ∀ (p : β),
    p ∈ s →
      ∀ (q : β),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → ↑↑μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p => ⋂ (q : β) (_ : q ∈ s ∩ Ioi p), u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x => ⨅ (i : ↑s), piecewise (u' ↑i) (fun x => ↑i) (fun x => ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), u' ↑p ∩ v ↑p ↑q
μt : ↑↑μ t ≤ 0
ff' : ∀ᵐ (x : α) ∂μ, f x = f' x
⊢ AEMeasurable f
[PROOFSTEP]
exact ⟨f', f'_meas, ff'⟩
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
⊢ AEMeasurable f
[PROOFSTEP]
obtain ⟨s, s_count, s_dense, _, s_top⟩ : ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s :=
  ENNReal.exists_countable_dense_no_zero_top
[GOAL]
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
⊢ AEMeasurable f
[PROOFSTEP]
have I : ∀ x ∈ s, x ≠ ∞ := fun x xs hx => s_top (hx ▸ xs)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
I : ∀ (x : ℝ≥0∞), x ∈ s → x ≠ ⊤
⊢ AEMeasurable f
[PROOFSTEP]
apply MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets μ s s_count s_dense _
[GOAL]
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
I : ∀ (x : ℝ≥0∞), x ∈ s → x ≠ ⊤
⊢ ∀ (p : ℝ≥0∞),
    p ∈ s →
      ∀ (q : ℝ≥0∞),
        q ∈ s →
          p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
[PROOFSTEP]
rintro p hp q hq hpq
[GOAL]
case intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
I : ∀ (x : ℝ≥0∞), x ∈ s → x ≠ ⊤
p : ℝ≥0∞
hp : p ∈ s
q : ℝ≥0∞
hq : q ∈ s
hpq : p < q
⊢ ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
[PROOFSTEP]
lift p to ℝ≥0 using I p hp
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
I : ∀ (x : ℝ≥0∞), x ∈ s → x ≠ ⊤
q : ℝ≥0∞
hq : q ∈ s
p : ℝ≥0
hp : ↑p ∈ s
hpq : ↑p < q
⊢ ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
[PROOFSTEP]
lift q to ℝ≥0 using I q hq
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
s : Set ℝ≥0∞
s_count : Set.Countable s
s_dense : Dense s
left✝ : ¬0 ∈ s
s_top : ¬⊤ ∈ s
I : ∀ (x : ℝ≥0∞), x ∈ s → x ≠ ⊤
p : ℝ≥0
hp : ↑p ∈ s
q : ℝ≥0
hq : ↑q ∈ s
hpq : ↑p < ↑q
⊢ ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ ↑↑μ (u ∩ v) = 0
[PROOFSTEP]
exact h p q (ENNReal.coe_lt_coe.1 hpq)
