refine ⟨fun h i _ j _ hij ↦ h i.prop j.prop (by rwa [Ne, Subtype.coe_injective.eq_iff]),
  fun h i hi j hj hij ↦ ?_⟩
case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
⊢ (↑u).PairwiseDisjoint s ↔ univ.PairwiseDisjoint fun i => s ↑i
case h.e'_2.a
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
u : Finset ι
s : ι → Set α
hs : ∀ i ∈ u, (s i).Finite
h : univ.PairwiseDisjoint fun i => s ↑i
i : ι
hi : i ∈ ↑u
j : ι
hj : j ∈ ↑u
hij : i ≠ j
⊢ (Disjoint on s) i j