α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
⊢ ↑↑μ
      ((if h : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then Exists.choose h
        else
          if h' : ∃ t_1 x, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t_1 ∩ u) = ↑↑μ (t ∩ u) then
            Exists.choose h'
          else Exists.choose (_ : ∃ t_1, t ⊆ t_1 ∧ MeasurableSet t_1 ∧ ↑↑μ t_1 = ↑↑μ t)) ∩
        s) =
    ↑↑μ (t ∩ s)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
⊢ ↑↑μ (toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)
rw [toMeasurable]
case inl
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ↑↑μ (Exists.choose (_ : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s) = ↑↑μ (t ∩ s)

case inr
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ¬∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ↑↑μ (Exists.choose A ∩ s) = ↑↑μ (t ∩ s)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
⊢ ↑↑μ
      ((if h : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then Exists.choose h
        else
          if h' : ∃ t_1 x, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t_1 ∩ u) = ↑↑μ (t ∩ u) then
            Exists.choose h'
          else Exists.choose (_ : ∃ t_1, t ⊆ t_1 ∧ MeasurableSet t_1 ∧ ↑↑μ t_1 = ↑↑μ t)) ∩
        s) =
    ↑↑μ (t ∩ s)
split_ifs with ht
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
let w n := toMeasurable μ (t ∩ v n)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
have hw : ∀ n, μ (w n) < ∞ := by
  intro n
  simp_rw [measure_toMeasurable]
  exact (h'v n).lt_top
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
set t' := ⋃ n, toMeasurable μ (t ∩ disjointed w n) with ht'
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
have tt' : t ⊆ t' :=
  calc
    t ⊆ ⋃ n, t ∩ disjointed w n := by
      rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
      intro x hx
      rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
      refine' mem_iUnion.2 ⟨n, _⟩
      have : x ∈ t ∩ v n := ⟨hx, hn⟩
      exact ⟨hx, subset_toMeasurable μ _ this⟩
    _ ⊆ ⋃ n, toMeasurable μ (t ∩ disjointed w n) :=
      iUnion_mono fun n => subset_toMeasurable _ _
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
⊢ ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
refine' ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => _⟩
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (t' ∩ u) ≤ ↑↑μ (t ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
apply le_antisymm _ (measure_mono (inter_subset_inter tt' Subset.rfl))
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
n : ℕ
⊢ ↑↑μ (w n) < ⊤
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
⊢ ∀ (n : ℕ), ↑↑μ (w n) < ⊤
intro n
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
n : ℕ
⊢ ↑↑μ (t ∩ v n) < ⊤
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
n : ℕ
⊢ ↑↑μ (w n) < ⊤
simp_rw [measure_toMeasurable]
no goals
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
n : ℕ
⊢ ↑↑μ (t ∩ v n) < ⊤
exact (h'v n).lt_top
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ (i : ℕ), t ∩ w i
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ (n : ℕ), t ∩ disjointed w n
rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
⊢ x ∈ ⋃ (i : ℕ), t ∩ w i
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ (i : ℕ), t ∩ w i
intro x hx
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ ⋃ (i : ℕ), t ∩ w i
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
⊢ x ∈ ⋃ (i : ℕ), t ∩ w i
rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ t ∩ w n
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ ⋃ (i : ℕ), t ∩ w i
refine' mem_iUnion.2 ⟨n, _⟩
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
this : x ∈ t ∩ v n
⊢ x ∈ t ∩ w n
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ t ∩ w n
have : x ∈ t ∩ v n := ⟨hx, hn⟩
no goals
case intro
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
this : x ∈ t ∩ v n
⊢ x ∈ t ∩ w n
exact ⟨hx, subset_toMeasurable μ _ this⟩
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (⋃ (i : ℕ), toMeasurable μ (t ∩ disjointed w i) ∩ u) ≤ ∑' (n : ℕ), ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (t' ∩ u) ≤ ∑' (n : ℕ), ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)
rw [ht', iUnion_inter]
no goals
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (⋃ (i : ℕ), toMeasurable μ (t ∩ disjointed w i) ∩ u) ≤ ∑' (n : ℕ), ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)
exact measure_iUnion_le _
case e_f
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n => ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)) = fun n => ↑↑μ (t ∩ disjointed w n ∩ u)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (∑' (n : ℕ), ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)) = ∑' (n : ℕ), ↑↑μ (t ∩ disjointed w n ∩ u)
congr 1
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) = ↑↑μ (t ∩ disjointed w n ∩ u)
case e_f
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n => ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u)) = fun n => ↑↑μ (t ∩ disjointed w n ∩ u)
ext1 n
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n) ≠ ⊤
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) = ↑↑μ (t ∩ disjointed w n ∩ u)
apply measure_toMeasurable_inter hu
case e_f.h.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n) < ⊤
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n) ≠ ⊤
apply ne_of_lt
no goals
case e_f.h.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n) < ⊤
calc
  μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) :=
    measure_mono (inter_subset_inter_right _ (disjointed_le w n))
  _ ≤ μ (w n) := (measure_mono (inter_subset_right _ _))
  _ < ∞ := hw n
case e_f
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n => ↑↑μ (t ∩ disjointed w n ∩ u)) = fun n => ↑↑(restrict μ (t ∩ u)) (disjointed w n)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (∑' (n : ℕ), ↑↑μ (t ∩ disjointed w n ∩ u)) = ∑' (n : ℕ), ↑↑(restrict μ (t ∩ u)) (disjointed w n)
congr 1
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n ∩ u) = ↑↑(restrict μ (t ∩ u)) (disjointed w n)
case e_f
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (fun n => ↑↑μ (t ∩ disjointed w n ∩ u)) = fun n => ↑↑(restrict μ (t ∩ u)) (disjointed w n)
ext1 n
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ ↑↑μ (t ∩ disjointed w n ∩ u) = ↑↑(restrict μ (t ∩ u)) (disjointed w n)
rw [restrict_apply, inter_comm t _, inter_assoc]
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n✝ n : ℕ
⊢ MeasurableSet (w n)
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)
refine MeasurableSet.disjointed (fun n => ?_) n
no goals
case e_f.h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n✝ n : ℕ
⊢ MeasurableSet (w n)
exact measurableSet_toMeasurable _ _
case hn
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on fun n => disjointed w n)

case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (∑' (n : ℕ), ↑↑(restrict μ (t ∩ u)) (disjointed w n)) = ↑↑(restrict μ (t ∩ u)) (⋃ (n : ℕ), disjointed w n)
rw [measure_iUnion]
no goals
case hn
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on fun n => disjointed w n)
exact disjoint_disjointed _
case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ MeasurableSet (disjointed w i)
case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ∀ (i : ℕ), MeasurableSet (disjointed w i)
intro i
case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i n : ℕ
⊢ MeasurableSet (w n)
case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ MeasurableSet (disjointed w i)
refine MeasurableSet.disjointed (fun n => ?_) i
no goals
case h
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i n : ℕ
⊢ MeasurableSet (w n)
exact measurableSet_toMeasurable _ _
no goals
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), ↑↑μ (w n) < ⊤
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict μ (t ∩ u)) univ = ↑↑μ (t ∩ u)
rw [restrict_apply MeasurableSet.univ, univ_inter]
case inl.H
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ Exists.choose (_ : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s
case inl
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ↑↑μ (Exists.choose (_ : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s) = ↑↑μ (t ∩ s)
apply measure_congr
no goals
case inl.H
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ Exists.choose (_ : ∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s
exact ae_eq_set_inter ht.choose_spec.snd.2 (ae_eq_refl _)
no goals
case inr
α : Type u_1
β : Type ?u.746309
γ : Type ?u.746312
δ : Type ?u.746315
ι : Type ?u.746318
R : Type ?u.746321
R' : Type ?u.746324
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤
A : ∃ t' x, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t' ∩ u) = ↑↑μ (t ∩ u)
ht : ¬∃ t_1 x, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ↑↑μ (Exists.choose A ∩ s) = ↑↑μ (t ∩ s)
exact A.choose_spec.snd.2 s hs