feat: port pi_fin.reflect instance (#3430)

This was skipped during the initial port of this file.

There are some golfing discussions [here on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unquoteExpr.3A.20inst.E2.9C.9D.C2.B2.2E2.20.3A.20Expr/near/349273797) that we could revisit later



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

Mathlib/Data/Fin/VecNotation.lean

@@ -11,6 +11,8 @@ Authors: Anne Baanen
 import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.List.Range
 import Mathlib.GroupTheory.GroupAction.Pi
+import Mathlib.Tactic.ToExpr
+import Qq
 
 /-!
 # Matrix and vector notation
@@ -199,31 +201,23 @@ theorem cons_fin_one (x : α) (u : Fin 0 → α) : vecCons x u = fun _ => x :=
   funext (cons_val_fin_one x u)
 #align matrix.cons_fin_one Matrix.cons_fin_one
 
--- Porting note: the next two decls are commented out. TODO(eric-wieser)
-
--- /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14:
---  unsupported tactic `reflect_name #[] -/
--- /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14:
---  unsupported tactic `reflect_name #[] -/
--- unsafe instance _root_.pi_fin.reflect [reflected_univ.{u}] [reflected _ α] [has_reflect α] :
---     ∀ {n}, has_reflect (Fin n → α)
---   | 0, v =>
---     (Subsingleton.elim vecEmpty v).rec
---       ((by
---             trace
---               "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14:
---                unsupported tactic `reflect_name #[]" :
---             reflected _ @vecEmpty.{u}).subst
---         q(α))
---   | n + 1, v =>
---     (cons_head_tail v).rec <|
---       (by
---             trace
---               "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14:
---                unsupported tactic `reflect_name #[]" :
---             reflected _ @vecCons.{u}).subst₄
---         q(α) q(n) q(_) (_root_.pi_fin.reflect _)
--- #align pi_fin.reflect pi_fin.reflect
+open Lean in
+open Qq in
+protected instance _root_.PiFin.toExpr [ToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α) :=
+  have lu := toLevel.{u}
+  have eα : Q(Type $lu) := toTypeExpr α
+  have toTypeExpr := q(Fin $n → $eα)
+  match n with
+  | 0 => { toTypeExpr, toExpr := fun _ => q(@vecEmpty $eα) }
+  | n + 1 =>
+    { toTypeExpr, toExpr := fun v =>
+      have := PiFin.toExpr n
+      have eh : Q($eα) := toExpr (vecHead v)
+      have et : Q(Fin $n → $eα) := toExpr (vecTail v)
+      q(vecCons $eh $et) }
+#align pi_fin.reflect PiFin.toExpr
+
+-- Porting note: the next decl is commented out. TODO(eric-wieser)
 
 -- /-- Convert a vector of pexprs to the pexpr constructing that vector.-/
 -- unsafe def _root_.pi_fin.to_pexpr : ∀ {n}, (Fin n → pexpr) → pexpr

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -947,9 +947,9 @@ theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : LocalHomeomorph
     (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
     _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
       EqOnSource.trans' (refl _) (EqOnSource.trans' (trans_self_symm _) (refl _))
-    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]; apply refl
+    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
     _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
-    _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]; apply refl
+    _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
   exact G.eq_on_source C (Setoid.symm D)
 #align structure_groupoid.compatible_of_mem_maximal_atlas StructureGroupoid.compatible_of_mem_maximalAtlas
 
@@ -1156,8 +1156,8 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') :
             (EqOnSource.trans' (trans_self_symm g) (_root_.refl _)))
         _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' :=
           by simp only [trans_assoc, _root_.refl]
-        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']; apply _root_.refl
-        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]; apply _root_.refl
+        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
+        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
         _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s :=
           by simp only [EqOnSource.restr, trans_assoc, _root_.refl]
         _ ≈ F₂ := by simp only [feq, _root_.refl]

test/vec_notation.lean

@@ -0,0 +1,30 @@
+/-
+Manually ported from
+https://github.com/leanprover-community/mathlib/blob/fee91d74414e681a8b72cb7160e6b5ef0ec2cc0b/test/vec_notation.lean
+-/
+import Mathlib.Data.Fin.VecNotation
+
+/-! These tests are testing `PiFin.toExpr` and fail with
+`local attribute [-instance] PiFin.toExpr` -/
+
+open Lean
+open Lean.Meta
+open Qq
+
+#eval do
+  let x : Fin 0 → ℕ := ![]
+  let .true ← isDefEq (toExpr x) q((![] : Fin 0 → ℕ)) | failure
+
+#eval do
+  let x := ![1, 2, 3]
+  let .true ← isDefEq (toExpr x) q(![1, 2, 3]) | failure
+
+#eval do
+  let x := ![![1, 2], ![3, 4]]
+  let .true ← isDefEq (toExpr x) q(![![1, 2], ![3, 4]]) | failure
+
+/-! These tests are testing `PiFin.repr` -/
+
+#eval show MetaM Unit from guard (toString (repr (![] : _ → ℕ)) = "![]")
+#eval show MetaM Unit from guard (toString (repr ![1, 2, 3]) = "![1, 2, 3]")
+#eval show MetaM Unit from guard (toString (repr ![![1, 2], ![3, 4]]) = "![![1, 2], ![3, 4]]")