case intro.intro
α : Type u_2
β : Type ?u.54235
γ : Type ?u.54238
ι✝ : Sort ?u.54241
ι' : Sort ?u.54244
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
I : Type u_1
l : I → Filter α
ι : I → Sort u_3
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : PairwiseDisjoint S l
hS : Set.Finite S
h : ∀ (i : I), HasBasis (l i) (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : PairwiseDisjoint S t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint S fun i => s i (ind i)
α : Type u_2
β : Type ?u.54235
γ : Type ?u.54238
ι✝ : Sort ?u.54241
ι' : Sort ?u.54244
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
I : Type u_1
l : I → Filter α
ι : I → Sort u_3
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : PairwiseDisjoint S l
hS : Set.Finite S
h : ∀ (i : I), HasBasis (l i) (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint S fun i => s i (ind i)
rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩
case intro.intro
α : Type u_2
β : Type ?u.54235
γ : Type ?u.54238
ι✝ : Sort ?u.54241
ι' : Sort ?u.54244
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
I : Type u_1
l : I → Filter α
ι : I → Sort u_3
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : PairwiseDisjoint S l
hS : Set.Finite S
h : ∀ (i : I), HasBasis (l i) (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : PairwiseDisjoint S t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint S fun i => s i (ind i)
case intro.intro
α : Type u_2
β : Type ?u.54235
γ : Type ?u.54238
ι✝ : Sort ?u.54241
ι' : Sort ?u.54244
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
I : Type u_1
l : I → Filter α
ι : I → Sort u_3
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : PairwiseDisjoint S l
hS : Set.Finite S
h : ∀ (i : I), HasBasis (l i) (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : PairwiseDisjoint S t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint S fun i => s i (ind i)
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
no goals
case intro.intro
α : Type u_2
β : Type ?u.54235
γ : Type ?u.54238
ι✝ : Sort ?u.54241
ι' : Sort ?u.54244
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
I : Type u_1
l : I → Filter α
ι : I → Sort u_3
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : PairwiseDisjoint S l
hS : Set.Finite S
h : ∀ (i : I), HasBasis (l i) (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : PairwiseDisjoint S t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ PairwiseDisjoint S fun i => s i (ind i)
exact ⟨ind, hp, hd.mono ht⟩