case refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter (fun k => {s k}) S → MeasurableSet t

case refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ {t | ∃ k, k ∈ S ∧ s k = t} ⊆ piiUnionInter (fun k => {s k}) S
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom {t | ∃ k, k ∈ S ∧ s k = t}
refine' le_antisymm (generateFrom_le _) (generateFrom_mono _)
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ I), f x)
case refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter (fun k => {s k}) S → MeasurableSet t
rintro _ ⟨I, hI, f, hf, rfl⟩
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k, k ∈ S ∧ s k = t}
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ I), f x)
refine' Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom _
no goals
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k, k ∈ S ∧ s k = t}
exact ⟨m, hI hm, (hf m hm).symm⟩
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k => {s k}) S
case refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ {t | ∃ k, k ∈ S ∧ s k = t} ⊆ piiUnionInter (fun k => {s k}) S
rintro _ ⟨k, hk, rfl⟩
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

case refine'_2.intro.intro.refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k => {s k}) i

case refine'_2.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ (x : ι) (_ : x ∈ {k}), s x
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k => {s k}) S
refine' ⟨{k}, fun m hm => _, s, fun i _ => _, _⟩
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S
rw [Finset.mem_coe, Finset.mem_singleton] at hm
no goals
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S
rwa [hm]
no goals
case refine'_2.intro.intro.refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k => {s k}) i
exact Set.mem_singleton _
no goals
case refine'_2.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ (x : ι) (_ : x ∈ {k}), s x
simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]