-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateFrom_piiUnionInter_singleton_left (s : ι → Set α) (S : Set ι) :
    generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom { t | ∃ k ∈ S, s k = t }

Proof state:
case refine_2.intro.intro.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

Tactic:
rw [Finset.mem_coe, Finset.mem_singleton] at hm

Result:
case refine_2.intro.intro.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S

Proof state:
case refine_2.intro.intro.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S

Tactic:
rwa [hm]

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k => {s k}) x
⊢ MeasurableSet (⋂ x ∈ I, f x)

Tactic:
refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_

Result:
case refine_1.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k => {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k ∈ S, s k = t}

Proof state:
case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k => {s k}) S

Tactic:
rintro _ ⟨k, hk, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k => {s k}) S

Proof state:
case refine_2.intro.intro.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x

Tactic:
simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k => {s k}) i

Tactic:
exact Set.mem_singleton _

Result:
no goals

Proof state:
case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k => {s k}) S, MeasurableSet t

Tactic:
rintro _ ⟨I, hI, f, hf, rfl⟩

Result:
case refine_1.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k => {s k}) x
⊢ MeasurableSet (⋂ x ∈ I, f x)

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ x ∈ I, f x ∈ (fun k => {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k ∈ S, s k = t}

Tactic:
exact ⟨m, hI hm, (hf m hm).symm⟩

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom {t | ∃ k ∈ S, s k = t}

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)

Result:
case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k => {s k}) S, MeasurableSet t

case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ {t | ∃ k ∈ S, s k = t} ⊆ piiUnionInter (fun k => {s k}) S

Proof state:
case refine_2.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k => {s k}) S

Tactic:
refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩

Result:
case refine_2.intro.intro.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

case refine_2.intro.intro.refine_2
α : Type u_3
ι : Type u_4
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_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x