How to show definitional equality

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

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

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

theorem Vector.allZero_def (v : Vector F n) : v.allZero = v.toList.all (.=0) := rfl

instance (v : Vector F n)  : Decidable (v.allZero) := inferInstance

structure ReducedRow0 (n : Nat)

structure ReducedRowN0 (n : Nat) where
  z : Fin n
  k : Nat
  tail : Vector F k
  h : n = p + k + 1

def ReducedRow (n : Nat) := Sum (ReducedRow0 n) (ReducedRowN0 F n)

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

def ReducedRow0.toVector (_ : ReducedRow0 n): Vector F n := zeroVec F n

def ReducedRowN0.toVector (row : ReducedRowN0 F n): Vector F n := row.h ▸ (zeroVec F n).append (Vector.cons 1 row.tail)

def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
  match row with
  | .inl row0 => row0.toVector F
  | .inr rowN0 => rowN0.toVector F

def ReducedRowN0.zerosAbove (row : ReducedRowN0 F n) (R : Vector (ReducedRowN0 F n) m) : Prop :=
  (R.map fun r => (r.toVector F).get row.z).allZero

section
variable (row : ReducedRowN0 F n) (R : Vector (ReducedRowN0 F n) m)

lemma myLemma_1 : ((R.map fun r => (r.toVector F).get row.z).toList.all (.=0)) = row.zerosAbove F R := rfl

instance : Decidable (row.zerosAbove F R) :=
  inferInstanceAs <| Decidable ((R.map fun r => (r.toVector F).get row.z).toList.all (.=0))

end

myLemma1 shows that the Decidable instance I want to make is definitionally equal to an already decidable instance. But Lean is not able to make this connection in the instance. How do I force the connection?

[Bbbbbbbbba]

This seems to do the trick:

instance t : Decidable (row.zerosAbove F R) :=
  inferInstanceAs <| Decidable (((R.map fun r => (r.toVector F).get row.z).toList.all (.=0)) = true)

[Vivek Rajesh Joshi]

Thanks!