use ⟨i, ⟨his, hi⟩⟩
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
s : Set α
i : α
his : i ∈ s
hi : ⟨i, his⟩ ∈ support fun a => f ↑a
⊢ ∃ a, (fun i => ⟨⟨↑i, ⋯⟩, ⋯⟩) a = ⟨⟨i, his⟩, hi⟩
no goals