case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t x, s' = ⋂ (i : ι) (_ : i ∈ t), s i}
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ piiUnionInter (fun i => {s i}) S = {s' | ∃ t x, s' = ⋂ (i : ι) (_ : i ∈ t), s i}
ext1 s'
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x) ↔
    ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t x, s' = ⋂ (i : ι) (_ : i ∈ t), s i}
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x
⊢ ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x) ↔
    ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
refine' ⟨fun h => _, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ ∃ t_1, ↑t_1 ⊆ S ∧ (⋂ (x : ι) (_ : x ∈ t), f x) = ⋂ (i : ι) (_ : i ∈ t_1), s i
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x
⊢ ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
obtain ⟨t, htS, f, hft_eq, rfl⟩ := h
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) = ⋂ (i : ι) (_ : i ∈ t), s i
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ ∃ t_1, ↑t_1 ⊆ S ∧ (⋂ (x : ι) (_ : x ∈ t), f x) = ⋂ (i : ι) (_ : i ∈ t_1), s i
refine' ⟨t, htS, _⟩
case h.intro.intro.intro.intro.h.e'_3.h.f
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ f x✝¹ = s x✝¹
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) = ⋂ (i : ι) (_ : i ∈ t), s i
congr! 3
case h.intro.intro.intro.intro.h.e'_3.h.f.a
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ x✝¹ ∈ t
case h.intro.intro.intro.intro.h.e'_3.h.f
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ f x✝¹ = s x✝¹
apply hft_eq
no goals
case h.intro.intro.intro.intro.h.e'_3.h.f.a
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ x✝¹ ∈ t
assumption