α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (t ∈ ⨅ (i : ι) (_ : i ∈ dom), l i) ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ HasBasis (⨅ (i : ι) (_ : i ∈ dom), l i) (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
refine' ⟨fun t => _⟩
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i, i ∈ dom ∧ t ∈ l i) ↔ ∃ a b, ((a, b).fst ∈ dom ∧ p (a, b).fst (a, b).snd) ∧ s (a, b).fst (a, b).snd ⊆ t
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (t ∈ ⨅ (i : ι) (_ : i ∈ dom), l i) ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t
rw [mem_biInf_of_directed h hdom, Prod.exists]
case refine'_1
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ i ∈ dom ∧ t ∈ l i → ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t

case refine'_2
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ (∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t) → i ∈ dom ∧ t ∈ l i
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i, i ∈ dom ∧ t ∈ l i) ↔ ∃ a b, ((a, b).fst ∈ dom ∧ p (a, b).fst (a, b).snd) ∧ s (a, b).fst (a, b).snd ⊆ t
refine' exists_congr fun i => ⟨_, _⟩
case refine'_1.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
hi : i ∈ dom
hti : t ∈ l i
⊢ ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t
case refine'_1
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ i ∈ dom ∧ t ∈ l i → ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t
rintro ⟨hi, hti⟩
case refine'_1.intro.intro.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
hi : i ∈ dom
hti : t ∈ l i
b : ι'
hb : p i b
hbt : s i b ⊆ t
⊢ ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t
case refine'_1.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
hi : i ∈ dom
hti : t ∈ l i
⊢ ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t
rcases(hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩
no goals
case refine'_1.intro.intro.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
hi : i ∈ dom
hti : t ∈ l i
b : ι'
hb : p i b
hbt : s i b ⊆ t
⊢ ∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t
exact ⟨b, ⟨hi, hb⟩, hbt⟩
case refine'_2.intro.intro.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι'
hibt : s (i, b).fst (i, b).snd ⊆ t
hi : (i, b).fst ∈ dom
hb : p (i, b).fst (i, b).snd
⊢ i ∈ dom ∧ t ∈ l i
case refine'_2
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ (∃ b, ((i, b).fst ∈ dom ∧ p (i, b).fst (i, b).snd) ∧ s (i, b).fst (i, b).snd ⊆ t) → i ∈ dom ∧ t ∈ l i
rintro ⟨b, ⟨hi, hb⟩, hibt⟩
no goals
case refine'_2.intro.intro.intro
α : Type u_3
β : Type ?u.37352
γ : Type ?u.37355
ι✝ : Sort ?u.37358
ι'✝ : Sort ?u.37361
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i✝ : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
dom : Set ι
hdom : Set.Nonempty dom
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι'
hibt : s (i, b).fst (i, b).snd ⊆ t
hi : (i, b).fst ∈ dom
hb : p (i, b).fst (i, b).snd
⊢ i ∈ dom ∧ t ∈ l i
exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩