no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.128695
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Finset α
h : Disjoint s t
⊢ Disjoint ↑s ↑t
exact_mod_cast h