case this
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s t : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∀ (i j : ι), i ≠ j → ∃ s t, Disjoint ↑s ↑t

α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s t : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this : ∀ (i j : ι), i ≠ j → ∃ s t, Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s t : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
have : ∀ i j, i ≠ j → ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s t : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this : ∀ (i j : ι), i ≠ j → ∃ s t, Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
choose! s t hst using this
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
i : ι
⊢ (fun i => ⋂ (j : ι), ↑(s i j) ∩ ↑(t j i)) i ∈ l i

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => ⋂ (j : ι), ↑(s i j) ∩ ↑(t j i)) i j
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
refine' ⟨fun i => ⋂ j, s i j ∩ t j i, fun i => _, fun i j hij => _⟩
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
i : ι
⊢ (fun i => ⋂ (j : ι), ↑(s i j) ∩ ↑(t j i)) i ∈ l i

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : (i : ι) → ι → { s // s ∈ l i }
t : ι → (j : ι) → { t // t ∈ l j }
hst : ∀ (i j : ι), i ≠ j → Disjoint ↑(s i j) ↑(t i j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => ⋂ (j : ι), ↑(s i j) ∩ ↑(t j i)) i j
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 _ _))]
no goals
case this
α : Type u
β : Type v
γ : Type w
δ : Type ?u.87127
ι✝ : Sort x
f g : Filter α
s t : Set α
ι : Type u_1
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∀ (i j : ι), i ≠ j → ∃ s t, Disjoint ↑s ↑t
simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd