chore: port fin.reflect (#3486)

This definition was deleted during porting.




Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Mathlib/Data/Fin/Basic.lean

@@ -14,6 +14,7 @@ import Mathlib.Order.RelIso.Basic
 import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Order.Hom.Set
 import Mathlib.Tactic.Set
+import Qq
 
 /-!
 # The finite type with `n` elements
@@ -2543,4 +2544,15 @@ protected theorem zero_mul [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by
 
 end Mul
 
+open Qq in
+instance toExpr (n : ℕ) : Lean.ToExpr (Fin n) where
+  toTypeExpr := q(Fin $n)
+  toExpr := match n with
+    | 0 => finZeroElim
+    | k + 1 => fun i => show Q(Fin $n) from
+      have i : Q(Nat) := Lean.mkNatLit i -- raw literal to avoid ofNat-double-wrapping
+      have : Q(NeZero $n) := haveI : $n =Q $k + 1 := ⟨⟩; by exact q(NeZero.succ)
+      q(OfNat.ofNat $i)
+#align fin.reflect Fin.toExprₓ
+
 end Fin