From 2dd3c9328d87ef2e13be47a1827533fc68e16253 Mon Sep 17 00:00:00 2001
From: Gabe <66077254+MrBrain295@users.noreply.github.com>
Date: Thu, 2 Apr 2026 22:09:27 -0500
Subject: [PATCH] Prove `Vect.map_cons`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

🌪️
Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 Core/Vec.lean | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/Core/Vec.lean b/Core/Vec.lean
index cdb7e1c..9f08ea7 100644
--- a/Core/Vec.lean
+++ b/Core/Vec.lean
@@ -222,12 +222,5 @@ intro i; simp [Vect.zip]
 theorem Vect.map_cons {f : Q -> P} {v : Vect n Q} {v' : Vect (n + 1) P} {q : Q} :
   v' = (λ i => f ((Vect.cons q v) i)) ->
   v' = Vect.cons (f q) (λ i => (f (v i))) := by
-intro h
-revert v' v;
-intro v
-apply v.induction
-case nil => simp
-case cons =>
-  intro n hd tl ih1
-  intro v' ih2
-  sorry
+intro h; subst h; funext i
+induction i using Fin.induction <;> simp [Vect.cons]