no goals
α : Type u_2
β : Type u_3
γ : Type ?u.28763
ι✝ : Sort ?u.28766
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
ι : Sort u_1
p : ι → Prop
s : ι → Set α
hf : HasBasis f p s
hh : Monotone h
t : Set β
⊢ (∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t
simp only [exists_const, true_and, comp]