Theorem: Finite.find_get (GMLInit/Class/Finite.lean)

State before:
α : Type u_1
inst : Finite α
i : Fin (Finite.size α)
⊢ find (Finite.get α i) = i
Tactic:
rw [find_eq_iff_get_eq]
State after:
no goals