exact ⟨a, mem_inter hxt ha, rfl⟩
case refine_1.intro.intro
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
a : α
ha : a ∈ s
hxt : f a ∈ t
⊢ f a ∈ f '' (f ⁻¹' t ∩ s)
no goals