-- Mathlib/MeasureTheory/PiSystem.lean
theorem piiUnionInter_singleton_left (s : ι → Set α) (S : Set ι) :
    piiUnionInter (fun i => ({s i} : Set (Set α))) S =
      { s' : Set α | ∃ (t : Finset ι) (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i }

Proof state:
case h.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
⊢ ∃ t_1, ↑t_1 ⊆ S ∧ ⋂ x ∈ t, f x = ⋂ i ∈ t_1, s i

Tactic:
refine ⟨t, htS, ?_⟩

Result:
case h.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
⊢ ⋂ x ∈ t, f x = ⋂ i ∈ t, s i

Proof state:
case h.intro.intro.intro.intro.h.e'_3.h.f
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ f x✝¹ = s x✝¹

Tactic:
apply hft_eq

Result:
case h.intro.intro.intro.intro.h.e'_3.h.f.a
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ x✝¹ ∈ t

Proof state:
case h.intro.intro.intro.intro.h.e'_3.h.f.a
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ x✝¹ ∈ t

Tactic:
assumption

Result:
no goals

Proof state:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x
⊢ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i

Tactic:
obtain ⟨t, htS, f, hft_eq, rfl⟩ := h

Result:
case h.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
⊢ ∃ t_1, ↑t_1 ⊆ S ∧ ⋂ x ∈ t, f x = ⋂ i ∈ t_1, s i

Proof state:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]

Result:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i

Proof state:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x) ↔ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i

Tactic:
refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩

Result:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ x ∈ t, f x = s x) ∧ s' = ⋂ x ∈ t, f x
⊢ ∃ t, ↑t ⊆ S ∧ s' = ⋂ i ∈ t, s i

Proof state:
case h.intro.intro.intro.intro
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
⊢ ⋂ x ∈ t, f x = ⋂ i ∈ t, s i

Tactic:
congr! 3

Result:
case h.intro.intro.intro.intro.h.e'_3.h.f
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ x ∈ t, f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ f x✝¹ = s x✝¹

Proof state:
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ piiUnionInter (fun i => {s i}) S = {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
ext1 s'

Result:
case h
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}