∀ {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter β) {x : Set α} (motive : x ∈ {s | ∃ t ∈ f, m ⁻¹' t ⊆ s} → Prop)
  (x_1 : x ∈ {s | ∃ t ∈ f, m ⁻¹' t ⊆ s}), (∀ (a' : Set β) (ha' : a' ∈ f) (ma'a : m ⁻¹' a' ⊆ x), motive ⋯) → motive x_1