[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)


[GOAL]
⊢ MeasurablePow ℝ≥0∞ ℝ
[PROOFSTEP]
refine' ⟨ENNReal.measurable_of_measurable_nnreal_prod _ _⟩
[GOAL]
case refine'_1
⊢ Measurable fun p => (↑p.fst, p.snd).fst ^ (↑p.fst, p.snd).snd
[PROOFSTEP]
simp_rw [ENNReal.coe_rpow_def]
[GOAL]
case refine'_1
⊢ Measurable fun p => if p.fst = 0 ∧ p.snd < 0 then ⊤ else ↑(p.fst ^ p.snd)
[PROOFSTEP]
refine' Measurable.ite _ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal
[GOAL]
case refine'_1
⊢ MeasurableSet {a | a.fst = 0 ∧ a.snd < 0}
[PROOFSTEP]
exact MeasurableSet.inter (measurable_fst (measurableSet_singleton 0)) (measurable_snd measurableSet_Iio)
[GOAL]
case refine'_2
⊢ Measurable fun x => (⊤, x).fst ^ (⊤, x).snd
[PROOFSTEP]
simp_rw [ENNReal.top_rpow_def]
[GOAL]
case refine'_2
⊢ Measurable fun x => if 0 < x then ⊤ else if x = 0 then 1 else 0
[PROOFSTEP]
refine' Measurable.ite measurableSet_Ioi measurable_const _
[GOAL]
case refine'_2
⊢ Measurable fun x => if x = 0 then 1 else 0
[PROOFSTEP]
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const


[GOAL]
M : Type ?u.4198
N : Type ?u.4201
α : Type ?u.4204
β : Type ?u.4214
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
⊢ ∀ (m : Mᵈᵐᵃ) (n : N) (a : α →ₘ[μ] β), m • n • a = n • m • a
[PROOFSTEP]
rintro _ _ ⟨_⟩
[GOAL]
case mk
M : Type ?u.4198
N : Type ?u.4201
α : Type ?u.4204
β : Type ?u.4214
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : SMul N β
inst✝ : ContinuousConstSMul N β
m✝ : Mᵈᵐᵃ
n✝ : N
a✝¹ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ m✝ • n✝ • Quot.mk Setoid.r a✝ = n✝ • m✝ • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl
[GOAL]
M : Type ?u.8732
N : Type ?u.8735
α : Type ?u.8738
β : Type ?u.8748
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
⊢ ∀ (a : Mᵈᵐᵃ) (x y : α →ₘ[μ] β), a • (x + y) = a • x + a • y
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
M : Type ?u.8732
N : Type ?u.8735
α : Type ?u.8738
β : Type ?u.8748
inst✝⁸ : MeasurableSpace M
inst✝⁷ : MeasurableSpace N
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : SMul M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : AddMonoid β
inst✝ : ContinuousAdd β
a✝² : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ a✝² • (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) = a✝² • Quot.mk Setoid.r a✝¹ + a✝² • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl
[GOAL]
M : Type ?u.19747
N : Type ?u.19750
α : Type ?u.19753
β : Type ?u.19763
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
⊢ ∀ (r : Mᵈᵐᵃ) (x y : α →ₘ[μ] β), r • (x * y) = r • x * r • y
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
M : Type ?u.19747
N : Type ?u.19750
α : Type ?u.19753
β : Type ?u.19763
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace N
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : Monoid M
inst✝⁴ : MulAction M α
inst✝³ : MeasurableSMul M α
inst✝² : SMulInvariantMeasure M α μ
inst✝¹ : Monoid β
inst✝ : ContinuousMul β
r✝ : Mᵈᵐᵃ
x✝ : α →ₘ[μ] β
a✝¹ : { f // AEStronglyMeasurable f μ }
y✝ : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ r✝ • (Quot.mk Setoid.r a✝¹ * Quot.mk Setoid.r a✝) = r✝ • Quot.mk Setoid.r a✝¹ * r✝ • Quot.mk Setoid.r a✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : Measurable fun x => ↑IsROrC.re (f x)
him : Measurable fun x => ↑IsROrC.im (f x)
⊢ Measurable f
[PROOFSTEP]
convert
  Measurable.add (M := 𝕜) (IsROrC.measurable_ofReal.comp hre) ((IsROrC.measurable_ofReal.comp him).mul_const IsROrC.I)
[GOAL]
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : Measurable fun x => ↑IsROrC.re (f x)
him : Measurable fun x => ↑IsROrC.im (f x)
x✝ : α
⊢ f x✝ = (IsROrC.ofReal ∘ fun x => ↑IsROrC.re (f x)) x✝ + (IsROrC.ofReal ∘ fun x => ↑IsROrC.im (f x)) x✝ * IsROrC.I
[PROOFSTEP]
exact (IsROrC.re_add_im _).symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable fun x => ↑IsROrC.re (f x)
him : AEMeasurable fun x => ↑IsROrC.im (f x)
⊢ AEMeasurable f
[PROOFSTEP]
convert
  AEMeasurable.add (M := 𝕜) (IsROrC.measurable_ofReal.comp_aemeasurable hre)
    ((IsROrC.measurable_ofReal.comp_aemeasurable him).mul_const IsROrC.I)
[GOAL]
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable fun x => ↑IsROrC.re (f x)
him : AEMeasurable fun x => ↑IsROrC.im (f x)
x✝ : α
⊢ f x✝ = (IsROrC.ofReal ∘ fun x => ↑IsROrC.re (f x)) x✝ + (IsROrC.ofReal ∘ fun x => ↑IsROrC.im (f x)) x✝ * IsROrC.I
[PROOFSTEP]
exact (IsROrC.re_add_im _).symm


[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
borelize G
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
haveI : SeparableSpace (Set.range f ∪ {0} : Set G) := hf_meas.separableSpace_range_union_singleton
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
⊢ 0 ∈ Set.range f ∪ {0}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ FinStronglyMeasurable f μ
[PROOFSTEP]
refine' ⟨fs, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤
[PROOFSTEP]
have h_fs_Lp : ∀ n, Memℒp (fs n) p μ := SimpleFunc.memℒp_approxOn_range hf_meas.measurable hf
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
h_fs_Lp : ∀ (n : ℕ), Memℒp (↑(fs n)) p
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤
[PROOFSTEP]
exact fun n => (fs n).measure_support_lt_top_of_memℒp (h_fs_Lp n) hp_ne_zero hp_ne_top
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
⊢ ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
[PROOFSTEP]
apply SimpleFunc.tendsto_approxOn
[GOAL]
case refine'_2.hx
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ f x ∈ closure (Set.range f ∪ {0})
[PROOFSTEP]
apply subset_closure
[GOAL]
case refine'_2.hx.a
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : Memℒp f p
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f (_ : Measurable f) (Set.range f ∪ {0}) 0 (_ : 0 ∈ Set.range f ∪ {0})
x : α
⊢ f x ∈ Set.range f ∪ {0}
[PROOFSTEP]
simp