tactic 'generalize' failed, result is not type correct

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

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

structure RowNz (F : Type) [Field F] [DecidableEq F] where
  z : Nat
  first_nz : F
  tail : List F
deriving Repr

def zeroRowNz (n : Nat) : List F := List.replicate n 0

def RowNz.toList (r : RowNz F) := (zeroRowNz r.z).append (r.first_nz::r.tail)

theorem RowNz.toList_NE (r : RowNz F) : r.toList.length ≠ 0 := by sorry

def List.toRowNz (l : List F) (hl : l.length ≠ 0) : RowNz F := sorry

theorem RowNz.toList_toRowNz_eq (r : RowNz F) : r.toList.toRowNz (r.toList_NE) = r := by
  unfold toList
  induction r.z with
  | zero => sorry
  | succ n ih => sorry

Why is Lean unable to generalize r.z here?

[Kyle Miller]

The expression r.z appears in the goal, but the types are constraining r.z to be r.z. You need to be able to change the z inside r simultaneously.

One way to accomplish that is to do cases on r first and then do induction on z. I'm using let and pattern matching here to do cases:

theorem RowNz.toList_toRowNz_eq (r : RowNz F) : r.toList.toRowNz (r.toList_NE) = r := by
  unfold toList
  let {z, first_nz, tail} := r
  induction z with
  | zero => sorry
  | succ n ih => sorry