α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
      ({ fst := a, snd := b }.fst ∈ dom ∧ p { fst := a, snd := b }.fst { fst := a, snd := b }.snd) ∧
        s { fst := a, snd := b }.fst { fst := a, snd := b }.snd ⊆ t
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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, Sigma.exists]
case refine'_1
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
      ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
        s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t

case refine'_2
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ (∃ b,
      ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
        s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t) →
    i ∈ dom ∧ t ∈ l i
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
      ({ fst := a, snd := b }.fst ∈ dom ∧ p { fst := a, snd := b }.fst { fst := a, snd := b }.snd) ∧
        s { fst := a, snd := b }.fst { fst := a, snd := b }.snd ⊆ t
refine' exists_congr fun i => ⟨_, _⟩
case refine'_1.intro
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
    ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
      s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
case refine'_1
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
      ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
        s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
rintro ⟨hi, hti⟩
case refine'_1.intro.intro.intro
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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
hb : p i b
hbt : s i b ⊆ t
⊢ ∃ b,
    ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
      s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
case refine'_1.intro
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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,
    ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
      s { fst := i, snd := b }.fst { fst := i, snd := 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.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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
hb : p i b
hbt : s i b ⊆ t
⊢ ∃ b,
    ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
      s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
exact ⟨b, ⟨hi, hb⟩, hbt⟩
case refine'_2.intro.intro.intro
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι' i
hibt : s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
hi : { fst := i, snd := b }.fst ∈ dom
hb : p { fst := i, snd := b }.fst { fst := i, snd := b }.snd
⊢ i ∈ dom ∧ t ∈ l i
case refine'_2
α : Type u_3
β : Type ?u.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
⊢ (∃ b,
      ({ fst := i, snd := b }.fst ∈ dom ∧ p { fst := i, snd := b }.fst { fst := i, snd := b }.snd) ∧
        s { fst := i, snd := b }.fst { fst := i, snd := 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.36496
γ : Type ?u.36499
ι✝ : Sort ?u.36502
ι'✝ : Sort ?u.36505
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 : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), i ∈ dom → HasBasis (l i) (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι' i
hibt : s { fst := i, snd := b }.fst { fst := i, snd := b }.snd ⊆ t
hi : { fst := i, snd := b }.fst ∈ dom
hb : p { fst := i, snd := b }.fst { fst := i, snd := b }.snd
⊢ i ∈ dom ∧ t ∈ l i
exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩