no goals
α : Type u_2
β : Type u_1
γ : Type ?u.52355
δ : Type ?u.52358
ε : Type ?u.52361
ι : Type ?u.52364
f✝ : α →. β
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ b ∈ toSubtype p f a ↔ ↑b = f a
rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]