exact ⟨fun i => g (fintypeEquivFin.symm i), by { simp[hf]; funext i; simp }⟩
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ∃ a,
    (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
      (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
no goals