α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val '' t)
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val '' t)
rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht
case refine'_1
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (t : Set ↑s),
    t ∈ {t | ∃ s', MeasurableSet s' ∧ Subtype.val ⁻¹' s' = t} → (fun t => NullMeasurableSet (Subtype.val '' t)) t

case refine'_2
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ (fun t => NullMeasurableSet (Subtype.val '' t)) ∅

case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (t : Set ↑s),
    (fun t => NullMeasurableSet (Subtype.val '' t)) t → (fun t => NullMeasurableSet (Subtype.val '' t)) (tᶜ)

case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (f : ℕ → Set ↑s),
    (∀ (n : ℕ), (fun t => NullMeasurableSet (Subtype.val '' t)) (f n)) →
      (fun t => NullMeasurableSet (Subtype.val '' t)) (⋃ (i : ℕ), f i)
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val '' t)
refine'
  generateFrom_induction (p := fun t : Set s => NullMeasurableSet ((↑) '' t) μ)
    { t : Set s | ∃ s' : Set α, MeasurableSet s' ∧ (↑) ⁻¹' s' = t } _ _ _ _ ht
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
s' : Set α
hs' : MeasurableSet s'
⊢ NullMeasurableSet (Subtype.val '' (Subtype.val ⁻¹' s'))
case refine'_1
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (t : Set ↑s),
    t ∈ {t | ∃ s', MeasurableSet s' ∧ Subtype.val ⁻¹' s' = t} → (fun t => NullMeasurableSet (Subtype.val '' t)) t
rintro t' ⟨s', hs', rfl⟩
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
s' : Set α
hs' : MeasurableSet s'
⊢ NullMeasurableSet (s' ∩ s)
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
s' : Set α
hs' : MeasurableSet s'
⊢ NullMeasurableSet (Subtype.val '' (Subtype.val ⁻¹' s'))
rw [Subtype.image_preimage_coe]
no goals
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s'✝ t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
s' : Set α
hs' : MeasurableSet s'
⊢ NullMeasurableSet (s' ∩ s)
exact hs'.nullMeasurableSet.inter hs
no goals
case refine'_2
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ (fun t => NullMeasurableSet (Subtype.val '' t)) ∅
simp only [image_empty, nullMeasurableSet_empty]
case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
t' : Set ↑s
⊢ (fun t => NullMeasurableSet (Subtype.val '' t)) t' → (fun t => NullMeasurableSet (Subtype.val '' t)) (t'ᶜ)
case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (t : Set ↑s),
    (fun t => NullMeasurableSet (Subtype.val '' t)) t → (fun t => NullMeasurableSet (Subtype.val '' t)) (tᶜ)
intro t'
case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
t' : Set ↑s
⊢ NullMeasurableSet (Subtype.val '' t') → NullMeasurableSet (s \ (fun a => ↑a) '' t')
case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
t' : Set ↑s
⊢ (fun t => NullMeasurableSet (Subtype.val '' t)) t' → (fun t => NullMeasurableSet (Subtype.val '' t)) (t'ᶜ)
simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
no goals
case refine'_3
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
t' : Set ↑s
⊢ NullMeasurableSet (Subtype.val '' t') → NullMeasurableSet (s \ (fun a => ↑a) '' t')
exact hs.diff
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), (fun t => NullMeasurableSet (Subtype.val '' t)) (f n)) →
    (fun t => NullMeasurableSet (Subtype.val '' t)) (⋃ (i : ℕ), f i)
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ∀ (f : ℕ → Set ↑s),
    (∀ (n : ℕ), (fun t => NullMeasurableSet (Subtype.val '' t)) (f n)) →
      (fun t => NullMeasurableSet (Subtype.val '' t)) (⋃ (i : ℕ), f i)
intro f
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n)) → NullMeasurableSet (Subtype.val '' ⋃ (i : ℕ), f i)
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), (fun t => NullMeasurableSet (Subtype.val '' t)) (f n)) →
    (fun t => NullMeasurableSet (Subtype.val '' t)) (⋃ (i : ℕ), f i)
dsimp only []
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n)) → NullMeasurableSet (⋃ (i : ℕ), Subtype.val '' f i)
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n)) → NullMeasurableSet (Subtype.val '' ⋃ (i : ℕ), f i)
rw [image_iUnion]
no goals
case refine'_4
α : Type u_1
β : Type ?u.253013
γ : Type ?u.253016
δ : Type ?u.253019
ι : Type ?u.253022
R : Type ?u.253025
R' : Type ?u.253028
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : Set ↑s
hs : NullMeasurableSet s
ht : MeasurableSet t
f : ℕ → Set ↑s
⊢ (∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n)) → NullMeasurableSet (⋃ (i : ℕ), Subtype.val '' f i)
exact NullMeasurableSet.iUnion