-- Mathlib/Order/Filter/Finite.lean
theorem mem_iInf_finset {s : Finset α} {f : α → Filter β} {t : Set β} :
    (t ∈ ⨅ a ∈ s, f a) ↔ ∃ p : α → Set β, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Proof state:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∀ (x : Subtype (Membership.mem s)), (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id x) = p x

Tactic:
rintro ⟨a, ha⟩

Result:
case refine_1.intro.intro.mk
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id ⟨a, ha⟩) = p ⟨a, ha⟩

Proof state:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']

Result:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ x, f ↑x ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

Proof state:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) a ∈ f a

Tactic:
simpa [ha] using hp ⟨a, ha⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ x, f ↑x ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Proof state:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∃ p_1, (∀ a ∈ s, p_1 a ∈ f a) ∧ ⋂ i, p i = ⋂ x, p_1 ↑x

Tactic:
refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
        fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩

Result:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ⋂ i, p i = ⋂ x, (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑x

Proof state:
case refine_2.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ a ∈ s, p a ∈ f a
⊢ ⋂ x, p ↑x ∈ ⨅ x, f ↑x

Tactic:
exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

Result:
no goals

Proof state:
case refine_1.intro.intro.mk
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id ⟨a, ha⟩) = p ⟨a, ha⟩

Tactic:
simp [ha]

Result:
no goals

Proof state:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

Tactic:
rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩

Result:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∃ p_1, (∀ a ∈ s, p_1 a ∈ f a) ∧ ⋂ i, p i = ⋂ x, p_1 ↑x

Proof state:
case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
rintro ⟨p, hpf, rfl⟩

Result:
case refine_2.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ a ∈ s, p a ∈ f a
⊢ ⋂ x, p ↑x ∈ ⨅ x, f ↑x

Proof state:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ⋂ i, p i = ⋂ x, (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑x

Tactic:
refine iInter_congr_of_surjective id surjective_id ?_

Result:
case refine_1.intro.intro
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∀ (x : Subtype (Membership.mem s)), (fun a => if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id x) = p x