Theorem: gimme_some_equiv (Jordan/Mathlib/Extensions.lean)

State before:
α : Type u_1
m : ℕ
inst✝ : Fintype α
hα : m = Fintype.card α
⊢ Nonempty (Fin m ≃ α)
Tactic:
exact ⟨(Fintype.equivFinOfCardEq hα.symm).symm⟩
State after:
no goals