Replace vector with same vector of equivalent length

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

variable {F : Type} [Field F] [DecidableEq F]

def Vector.any {F : Type} (v : Vector F n) (p : F → Bool) := v.toList.any p

@[simp] theorem Vector.any_def (v : Vector F n) (p : F → Bool) : v.any p = v.toList.any p := rfl

def Vector.firstNonzElt {F : Type} [Field F] [DecidableEq F] (v : Vector F n) (h: v.any (· ≠ 0)) : {x:F // x≠0}×(i : Fin n)×(Vector F (n-i-1)) :=
  match v with
  | ⟨[],hv⟩ => by simp at h
  | ⟨x::ys,ha⟩ =>
    have hn : n > 0 := by rw [← ha]; simp
    if hx:x ≠ 0
    then (⟨x, hx⟩, ⟨⟨0,hn⟩,⟨ys,by simp_rw [← ha];simp⟩⟩)
    else
      by
      have ys_nontriv: ys.any (· ≠ 0) := by
        simp at hx
        simp [List.any_cons, hx] at h
        simp [h]
      let (value, ⟨index, tail⟩) := firstNonzElt (⟨ys,by simp at ha; rw [← ha]; simp⟩ : Vector F (n-1)) ys_nontriv
      exact (value, ⟨index.succ.cast (by simp [Nat.sub_add_cancel hn]),tail.congr (by simp [Nat.Simproc.sub_add_eq_comm n (↑index) 1])⟩)

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

theorem Vector.append_def {n m : Nat} (v : Vector α n) (w : Vector α m) :
  v.append w = ⟨v.toList++w.toList,by simp⟩ := rfl

lemma Vector.firstNonzElt_zeroVecAppend {p : Nat} {w : Vector F n} (hw : w.any (.≠0)) :
  (((zeroVec p).append w).firstNonzElt (by simp at hw ⊢; rcases hw with ⟨x,hx⟩; use x; exact ⟨Or.inr hx.1,hx.2⟩)).1 = (w.firstNonzElt hw).1 := by
  induction p with
  | zero => simp [zeroVec,replicate,append_def]; have := w.mk_toList (w.toList_length); rw [this]
  | succ n ih => sorry

How can I get rw [this] to work here?
I am aware of Vector.congr, but that's not what I want. I want something that is able to substitute one equivalent vector for another, not convert one to the other.

[Daniel Weber]

congr 1
· rw [zero_add]
· congr 1
  · simp
  convert heq_of_eq this
  rw [zero_add]; rfl
  apply zero_add

works

[Vivek Rajesh Joshi]

Ahh right, the congr tactic. Thanks a lot!!

[Vivek Rajesh Joshi]

Same problem with the succ case, although I can't use congr here:

| succ n ih =>
    simp [zeroVec,replicate,append_def] at ih ⊢
    rw [cons_eq_listCons 0 (List.replicate n 0 ++ w.toList)]