case a
α : Type u_1
β : Type ?u.11236
γ : Type ?u.11239
ι : Sort u_2
ι' : Sort ?u.11245
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 ↔ t ∈ l'
α : Type u_1
β : Type ?u.11236
γ : Type ?u.11239
ι : Sort u_2
ι' : Sort ?u.11245
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
⊢ l = l'
ext t
no goals
case a
α : Type u_1
β : Type ?u.11236
γ : Type ?u.11239
ι : Sort u_2
ι' : Sort ?u.11245
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 ↔ t ∈ l'
rw [hl.mem_iff, hl'.mem_iff]