chore(Data/Vector): golf ofFn_get

[euprunin]

---

Show trace profiling of ofFn_get: <10 ms before, <10 ms after 🎉

Trace profiling of ofFn_get before PR 32113

diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 62c8ebae5a..b259fba975 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -162,6 +162,7 @@ theorem map₂_cons (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vec
 theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f i := by
   simp [get_eq_get_toList]
 
+set_option trace.profiler true in
 @[simp]
 theorem ofFn_get (v : Vector α n) : ofFn (get v) = v := by
   rcases v with ⟨l, rfl⟩

✔ [566/566] Built Mathlib.Data.Vector.Basic (1.3s)
Build completed successfully (566 jobs).

Trace profiling of ofFn_get after PR 32113

diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 62c8ebae5a..bacb996e45 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -162,12 +162,11 @@ theorem map₂_cons (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vec
 theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f i := by
   simp [get_eq_get_toList]
 
+set_option trace.profiler true in
 @[simp]
 theorem ofFn_get (v : Vector α n) : ofFn (get v) = v := by
-  rcases v with ⟨l, rfl⟩
-  apply toList_injective
-  dsimp
-  simpa only [toList_ofFn] using List.ofFn_get _
+  ext
+  apply List.Vector.get_ofFn
 
 /-- The natural equivalence between length-`n` vectors and functions from `Fin n`. -/
 def _root_.Equiv.vectorEquivFin (α : Type*) (n : ℕ) : Vector α n ≃ (Fin n → α) :=

✔ [566/566] Built Mathlib.Data.Vector.Basic (1.3s)
Build completed successfully (566 jobs).

---

[github-actions]

PR summary 09610fd365

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).