-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_biInf_of_directed' {ι : Type*} {ι' : ι → Sort _} {dom : Set ι}
    (hdom : dom.Nonempty) {l : ι → Filter α} (s : ∀ i, ι' i → Set α) (p : ∀ i, ι' i → Prop)
    (hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) :
    (⨅ i ∈ dom, l i).HasBasis (fun ii' : Σi, ι' i => ii'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' =>
      s ii'.1 ii'.2

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι' i
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

Tactic:
exact ⟨hi, (hl i hi).mem_iff.mpr ⟨b, hb, hibt⟩⟩

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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

Tactic:
rcases (hl i hi).mem_iff.mp hti with ⟨b, hb, hbt⟩

Result:
case refine_1.intro.intro.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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, (⟨i, b⟩.fst ∈ dom ∧ p ⟨i, b⟩.fst ⟨i, b⟩.snd) ∧ s ⟨i, b⟩.fst ⟨i, b⟩.snd ⊆ t

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ 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

Tactic:
refine exists_congr fun i => ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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

Proof state:
case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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

Tactic:
rintro ⟨hi, hti⟩

Result:
case refine_1.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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, (⟨i, b⟩.fst ∈ dom ∧ p ⟨i, b⟩.fst ⟨i, b⟩.snd) ∧ s ⟨i, b⟩.fst ⟨i, b⟩.snd ⊆ t

Tactic:
exact ⟨b, ⟨hi, hb⟩, hbt⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (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

Tactic:
rintro ⟨b, ⟨hi, hb⟩, hibt⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
i : ι
b : ι' i
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

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t

Tactic:
rw [mem_biInf_of_directed h hdom, Sigma.exists]

Result:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ 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

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ (⨅ i ∈ dom, l i).HasBasis (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

Tactic:
refine ⟨fun t => ?_⟩

Result:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t