μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
let T : s × s → Set ℝ := fun p => Ioo p.1 p.2
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
let u := ⋃ i : ↥s × ↥s, T i
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
obtain ⟨A, A_count, hA⟩ :
  ∃ A : Set (↥s × ↥s), A.Countable ∧ (⋃ i ∈ A, T i) = ⋃ i : ↥s × ↥s, T i :=
  isOpen_iUnion_countable _ fun p => isOpen_Ioo
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p), p x
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, p x
apply ae_restrict_of_ae_restrict_of_subset this
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ (∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x) ∧ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p), p x
rw [ae_restrict_union_iff, ae_restrict_biUnion_iff _ A_count]
case intro.intro.left
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x

case intro.intro.right
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
case intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ (∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x) ∧ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
constructor
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
⊢ s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
intro x hx
case pos
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p

case neg
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : ¬x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
case pos
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
case pos
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
rw [← hA] at h'x
case pos.intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
case pos
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
  simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
case pos.intro.intro.h
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
case pos.intro.intro
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
right
no goals
case pos.intro.intro.h
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
exact mem_biUnion pA ⟨hx, xp⟩
no goals
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i
⊢ ∃ p, p ∈ A ∧ x ∈ T p
simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
no goals
case neg
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
x : ℝ
hx : x ∈ s
h'x : ¬x ∈ ⋃ (i : ↑s × ↑s), T i
⊢ x ∈ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
exact Or.inl ⟨hx, h'x⟩
case intro.intro.left
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this✝ : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
this : Measure.restrict μ (s \ u) = 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x
case intro.intro.left
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x
have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
no goals
case intro.intro.left
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this✝ : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
this : Measure.restrict μ (s \ u) = 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s \ u), p x
simp only [this, ae_zero, eventually_bot]
no goals
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ Measure.restrict μ (s \ u) = 0
simp only [restrict_eq_zero, hfinite.measure_zero]
case intro.intro.right.mk.mk.mk
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T ({ val := a, property := as }, { val := b, property := bs })), p x
case intro.intro.right
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
⊢ ∀ (i : ↑s × ↑s), i ∈ A → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T i), p x
rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
case intro.intro.right.mk.mk.mk
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
case intro.intro.right.mk.mk.mk
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ T ({ val := a, property := as }, { val := b, property := bs })), p x
dsimp
case intro.intro.right.mk.mk.mk.inl
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x

case intro.intro.right.mk.mk.mk.inr
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
case intro.intro.right.mk.mk.mk
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
rcases le_or_lt b a with (hba | hab)
no goals
case intro.intro.right.mk.mk.mk.inl
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hba : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
simp only [Ioo_eq_empty_of_le hba, inter_empty, restrict_empty, ae_zero, eventually_bot]
no goals
case intro.intro.right.mk.mk.mk.inr
μ : MeasureTheory.Measure ℝ
inst✝ : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p => Ioo ↑p.fst ↑p.snd
u : Set ℝ := ⋃ (i : ↑s × ↑s), T i
hfinite : Set.Finite (s \ u)
A : Set (↑s × ↑s)
A_count : Set.Countable A
hA : (⋃ (i : ↑s × ↑s) (_ : i ∈ A), T i) = ⋃ (i : ↑s × ↑s), T i
this : s ⊆ s \ u ∪ ⋃ (p : ↑s × ↑s) (_ : p ∈ A), s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
hab : a < b
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ (s ∩ Ioo a b), p x
exact h a b as bs hab