Substitution for equivalent types

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

structure ReducedRow (n : Nat) where
  z : Fin n
  k : Nat
  tail : Vector Rat k
  h : n = z + k + 1

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

def ReducedRow.toVector (row : ReducedRow n): Vector Rat (n) :=
  row.h ▸ (zeroVec row.z).append (Vector.cons 1 row.tail)

inductive RowEchelonForm : Nat → Nat → Type where
| row1 {n : Nat} (row : ReducedRow n) : RowEchelonForm 1 n
| rowAppend (row : ReducedRow n) {m : Nat} (rowlist : RowEchelonForm m n) : RowEchelonForm (m+1) n

#check finOneEquiv

def RowEchelonForm.toMatrix (R : RowEchelonForm m n) : Matrix (Fin m) (Fin n) Rat :=
  match R with
  | row1 row =>  Matrix.row row.toVector.get

In this code, I want to substitute Unit with Fin 1 in the type for the last line. How do I do this?

[Yakov Pechersky]

On the most recent mathlib, Matrix.row works across unique types. Can you try updating?

[Vivek Rajesh Joshi]

I've updated it to 4.9.0-rc3, and it's still flagging the line, but it now gives a different error message:

application type mismatch
  Matrix.row row.toVector.get
argument
  row.toVector.get
has type
  Fin n → ℚ : Type
but is expected to have type
  Type ?u.6899 : Type (?u.6899 + 1)

[Jireh Loreaux]

But did you update Mathlib?

[Vivek Rajesh Joshi]

Yes, the lean-toolchain file for Mathlib also reads 4.9.0-rc3

[Ruben Van de Velde]

Yeah, row now takes an extra argument. Try adding an underscore after row

[Vivek Rajesh Joshi]

Yes, that works. Thanks!