α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
haveI := ht.to_subtype
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : ↑t → Set α
hsl : ∀ (i : ↑t), s i ∈ l ↑i
hsd : Pairwise (Disjoint on s)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : (i : ↑t) → { s // s ∈ l ↑i }
hsd : Pairwise (Disjoint on fun i => ↑(s i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
case intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : ↑t → Set α
hsl : ∀ (i : ↑t), s i ∈ l ↑i
hsd : Pairwise (Disjoint on s)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
lift s to (i : t) → {s // s ∈ l i} using hsl
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : (i : ι) → { s // s ∈ l i }
hsd : Pairwise (Disjoint on fun i => ↑((fun i => s ↑i) i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : (i : ↑t) → { s // s ∈ l ↑i }
hsd : Pairwise (Disjoint on fun i => ↑(s i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.89945
ι✝ : Sort x
f g : Filter α
s✝ t✝ : Set α
ι : Type u_1
l : ι → Filter α
t : Set ι
hd : PairwiseDisjoint t l
ht : Set.Finite t
this : Finite ↑t
s : (i : ι) → { s // s ∈ l i }
hsd : Pairwise (Disjoint on fun i => ↑((fun i => s ↑i) i))
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ PairwiseDisjoint t s
exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩