Manually simplify match tactic

Stream: new members

[Vivek Rajesh Joshi]

How do I manually simplify the match tactic for row.z here?

import Mathlib.Data.Matrix.Notation

variable (F : Type) [Field F] [DecidableEq F] [Repr F]

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

instance [DecidableEq α] (a : α) (v : Vector α n) : Decidable (a ∈ v) :=
  inferInstanceAs <| Decidable (a ∈ v.toList)

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

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

abbrev Vector.allZero (v : Vector F n) : Prop := v.toList.all (.=0)

def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
  match hz:row.z with
  | none => zeroVec F n
  | some p => row.h hz ▸ (zeroVec F p).append (Vector.cons 1 row.tail)

example (row : ReducedRow F n) (hrow : ¬(row.toVector F).allZero) : row.z.isSome := by
  dsimp at hrow
  rw [ReducedRow.toVector] at hrow
  match hz : row.z with
  | none =>
    simp [hz] at hrow
  | some rz => sorry

[Bbbbbbbbba]

Do you have problems with the first branch of the match or the second?

[Vivek Rajesh Joshi]

The none branch

[Bbbbbbbbba]

lean3 - What does the "motive is not type correct" error mean in Lean? - Proof Assistants Stack Exchange
I could only find this for now

[Bbbbbbbbba]

My understanding is that trying to rewrite with hz makes Lean confused with row.h somehow