α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
⊢ ∀ (t : Set α), t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
intro t
case mp
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

case mpr
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
constructor
case mp
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ (∃ t₁, (∃ i, p i ∧ s i ⊆ t₁) ∧ ∃ t₂, (∃ i, p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
    ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
case mp
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i'✝ : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'
case mp
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ (∃ t₁, (∃ i, p i ∧ s i ⊆ t₁) ∧ ∃ t₂, (∃ i, p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
    ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i'✝ : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'
exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩
case mpr.intro.mk.intro.intro
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i'✝ : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
i : ι
i' : ι'
H : s { fst := i, snd := i' }.fst ∩ s' { fst := i, snd := i' }.snd ⊆ t
hi : p { fst := i, snd := i' }.fst
hi' : p' { fst := i, snd := i' }.snd
⊢ t ∈ l ⊓ l'
case mpr
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
rintro ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩
no goals
case mpr.intro.mk.intro.intro
α : Type u_1
β : Type ?u.29550
γ : Type ?u.29553
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i✝ : ι
p' : ι' → Prop
s' : ι' → Set α
i'✝ : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
t : Set α
i : ι
i' : ι'
H : s { fst := i, snd := i' }.fst ∩ s' { fst := i, snd := i' }.snd ⊆ t
hi : p { fst := i, snd := i' }.fst
hi' : p' { fst := i, snd := i' }.snd
⊢ t ∈ l ⊓ l'
exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H