α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
⊢ (t ∈ ⨅ (x : { i // i ∈ s }), f ↑x) ↔ ∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
⊢ (t ∈ ⨅ (a : α) (_ : a ∈ s), f a) ↔ ∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (a : α) (_ : a ∈ s), p a
simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x) → t ∈ ⨅ (x : { i // i ∈ s }), f ↑x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
⊢ (t ∈ ⨅ (x : { i // i ∈ s }), f ↑x) ↔ ∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x
refine' ⟨fun h => _, _⟩
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∃ p_1, (∀ (a : α), a ∈ s → p_1 a ∈ f a) ∧ (⋂ (i : { i // i ∈ s }), p i) = ⋂ (x : ↑↑s), p_1 ↑x
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x
rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ (⋂ (i : { i // i ∈ s }), p i) = ⋂ (x : ↑↑s), (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑x
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∃ p_1, (∀ (a : α), a ∈ s → p_1 a ∈ f a) ∧ (⋂ (i : { i // i ∈ s }), p i) = ⋂ (x : ↑↑s), p_1 ↑x
refine'
  ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ, fun a ha => by simpa [ha] using hp ⟨a, ha⟩, _⟩
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∀ (x : { i // i ∈ s }), (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑(id x) = p x
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ (⋂ (i : { i // i ∈ s }), p i) = ⋂ (x : ↑↑s), (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑x
refine' iInter_congr_of_surjective id surjective_id _
case refine'_1.intro.intro.mk
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑(id { val := a, property := ha }) =
    p { val := a, property := ha }
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
⊢ ∀ (x : { i // i ∈ s }), (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑(id x) = p x
rintro ⟨a, ha⟩
no goals
case refine'_1.intro.intro.mk
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p { val := a, property := h } else univ) ↑(id { val := a, property := ha }) =
    p { val := a, property := ha }
simp [ha]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : { i // i ∈ s } → Set β
hp : ∀ (i : { i // i ∈ s }), p i ∈ f ↑i
h : (⋂ (i : { i // i ∈ s }), p i) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p { val := a, property := h } else univ) a ∈ f a
simpa [ha] using hp ⟨a, ha⟩
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ (a : α), a ∈ s → p a ∈ f a
⊢ (⋂ (x : ↑↑s), p ↑x) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (x : ↑↑s), p ↑x) → t ∈ ⨅ (x : { i // i ∈ s }), f ↑x
rintro ⟨p, hpf, rfl⟩
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.107252
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ (a : α), a ∈ s → p a ∈ f a
⊢ (⋂ (x : ↑↑s), p ↑x) ∈ ⨅ (x : { i // i ∈ s }), f ↑x
exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)