-- Mathlib/Order/Filter/Finite.lean
theorem _root_.Pairwise.exists_mem_filter_of_disjoint {ι : Type*} [Finite ι] {l : ι → Filter α}
    (hd : Pairwise (Disjoint on l)) :
    ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ Pairwise (Disjoint on s)

Proof state:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
  simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd

Result:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this : Pairwise fun i j => ∃ s t, Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Proof state:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ Pairwise fun i j => ∃ s t, Disjoint ↑s ↑t

Tactic:
simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd

Result:
no goals

Proof state:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this : Pairwise fun i j => ∃ s t, Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
choose! s t hst using this

Result:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Proof state:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩

Result:
case refine_1
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i : ι
⊢ (fun i => ⋂ j, ↑s ∩ ↑t) i ∈ l i

case refine_2
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => ⋂ j, ↑s ∩ ↑t) i j

Proof state:
case refine_1
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i : ι
⊢ (fun i => ⋂ j, ↑s ∩ ↑t) i ∈ l i

case refine_2
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => ⋂ j, ↑s ∩ ↑t) i j

Tactic:
exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
  (hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
    ((iInter_subset _ i).trans inter_subset_right)]

Result:
no goals