simpa using hij
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
hi : i ∈ s ∩ support f
j : α
hj : j ∈ s ∩ support f
hij : (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨i, hi⟩ = (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
no goals