α : Type u_2
β : Type u_1
γ : Type ?u.73849
ι : Sort ?u.73852
ι' : Sort ?u.73855
f✝ : ι → α
s t✝ : Set α
f : α → β
t : Set β
x : β
x✝ : x ∈ t ∩ range f
hx : x ∈ t
y : α
h_eq : f y = x
⊢ x ∈ t
α : Type u_2
β : Type u_1
γ : Type ?u.73849
ι : Sort ?u.73852
ι' : Sort ?u.73855
f✝ : ι → α
s t✝ : Set α
f : α → β
t : Set β
x : β
x✝ : x ∈ t ∩ range f
hx : x ∈ t
y : α
h_eq : f y = x
⊢ y ∈ f ⁻¹' t
rw [preimage, mem_setOf, h_eq]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.73849
ι : Sort ?u.73852
ι' : Sort ?u.73855
f✝ : ι → α
s t✝ : Set α
f : α → β
t : Set β
x : β
x✝ : x ∈ t ∩ range f
hx : x ∈ t
y : α
h_eq : f y = x
⊢ x ∈ t
exact hx