α : Type u_1
β : Type ?u.22063
γ : Type ?u.22066
ι : Sort ?u.22069
ι' : Sort ?u.22072
l✝ l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i, i ∈ l ∧ P i ∧ i ⊆ t) ↔ ∀ (t : Set α), t ∈ l → ∃ r, r ∈ l ∧ P r ∧ r ⊆ t
α : Type u_1
β : Type ?u.22063
γ : Type ?u.22066
ι : Sort ?u.22069
ι' : Sort ?u.22072
l✝ l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
l : Filter α
P : Set α → Prop
⊢ HasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ (t : Set α), t ∈ l → ∃ r, r ∈ l ∧ P r ∧ r ⊆ t
simp only [hasBasis_iff, id, and_assoc]
no goals
α : Type u_1
β : Type ?u.22063
γ : Type ?u.22066
ι : Sort ?u.22069
ι' : Sort ?u.22072
l✝ l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i, i ∈ l ∧ P i ∧ i ⊆ t) ↔ ∀ (t : Set α), t ∈ l → ∃ r, r ∈ l ∧ P r ∧ r ⊆ t
exact forall_congr' fun s =>
  ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩