no goals
α✝ : Type ?u.21646
β✝ : Type ?u.21649
γ : Type ?u.21652
ι : Type ?u.21655
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton α
f : α → β
x y : α
⊢ f x = f y
rw [Subsingleton.elim x y]