simpa using hne
α : Type u_1
β : Type u_2
s✝ t✝ : Set α
n : ℕ
ι : Type u_3
s : ι → Set α
t : Finset ι
ht : (↑t).PairwiseDisjoint s
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
hne : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ i ≠ j
no goals