simp [hs hi hj hij]
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝² : Infinite ↑a
x✝¹ x✝ : ↑a
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
hij : s ↑⟨i, hi⟩ = s ↑⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
no goals