case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
⊢ piiUnionInter π {i} = π i ∪ {univ}
ext1 s
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} ↔ s ∈ π i ∨ s ∈ {univ}
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
simp only [piiUnionInter, exists_prop, mem_union]
case h.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} → s ∈ π i ∨ s ∈ {univ}

case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} ↔ s ∈ π i ∨ s ∈ {univ}
refine' ⟨_, fun h => _⟩
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : ↑t ⊆ {i}
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
case h.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} → s ∈ π i ∨ s ∈ {univ}
rintro ⟨t, hti, f, hfπ, rfl⟩
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : ↑t ⊆ {i}
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
simp only [subset_singleton_iff, Finset.mem_coe] at hti
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}

case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
by_cases hi : i ∈ t
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
have ht_eq_i : t = {i} := by
  ext1 x
  rw [Finset.mem_singleton]
  exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
no goals
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}
exact Or.inl (hfπ i hi)
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ {i}
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
⊢ t = {i}
ext1 x
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x = i
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ {i}
rw [Finset.mem_singleton]
no goals
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x = i
exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
ht_empty : t = ∅
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
have ht_empty : t = ∅ := by
  ext1 x
  simp only [Finset.not_mem_empty, iff_false_iff]
  exact fun hx => hi (hti x hx ▸ hx)
no goals
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
ht_empty : t = ∅
⊢ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ π i ∨ (⋂ (x : ι) (_ : x ∈ t), f x) ∈ {univ}
simp [ht_empty, Finset.not_mem_empty, iInter_false, iInter_univ, Set.mem_singleton univ,
  or_true_iff]
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ ∅
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
⊢ t = ∅
ext1 x
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ ¬x ∈ t
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ ∅
simp only [Finset.not_mem_empty, iff_false_iff]
no goals
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ ¬x ∈ t
exact fun hx => hi (hti x hx ▸ hx)
case h.refine'_2.inl
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}

case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
cases' h with hs hs
case h.refine'_2.inl.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}

case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x => s) x ∈ π x

case h.refine'_2.inl.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ (x : ι) (_ : x ∈ {i}), (fun x => s) x
case h.refine'_2.inl
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
refine' ⟨{i}, _, fun _ => s, ⟨fun x hx => _, _⟩⟩
no goals
case h.refine'_2.inl.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}
rw [Finset.coe_singleton]
case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
⊢ (fun x => s) x ∈ π x
case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x => s) x ∈ π x
rw [Finset.mem_singleton] at hx
no goals
case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
⊢ (fun x => s) x ∈ π x
rwa [hx]
no goals
case h.refine'_2.inl.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ (x : ι) (_ : x ∈ {i}), (fun x => s) x
simp only [Finset.mem_singleton, iInter_iInter_eq_left]
case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ ↑∅ ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ ∅ → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ ∅), f x
case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
refine' ⟨∅, _⟩
no goals
case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ ↑∅ ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ ∅ → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ ∅), f x
simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
  imp_true_iff, Finset.not_mem_empty, iInter_false, iInter_univ, true_and_iff,
  exists_const] using hs