how to prove the execution result of def = def

Stream: new members

[Alex]

I want to use Lean to prove that the execution result of Gaussian elimination is a RowEchelonForm matrix. Is this possible?And what should I do? Thanks very much!

import Mathlib
universe u
variable {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
def row_index_col_max_abs_arg  {m n : ℕ } (A : Matrix (Fin m) (Fin n) R) (i : Fin m ) (j : Fin n ) :Option (Fin m)  :=
  --List.argmax (f := fun i => abs (A i j)) (l := (Finset.univ.sort (· ≤ ·)).filter ) -- l = [i,...,m]
  List.argmax (f := fun i => abs (A i j)) (l := (Finset.filter (fun ti => ti ≥ i) (Finset.univ)).sort (· ≤ ·) )-- l = [i,...,m]

def elementary_row_switch {tm tn : Type u} [Fintype tm] [DecidableEq tm][DecidableEq tn] [Fintype tn](A : Matrix tm tn R) (i j : tm ): Matrix tm tn R :=
  fun (r : tm ) => if r = i then A j  else
                        if r = j then A i else
                        A r
def elementary_row_addition {tm tn : Type u} [Fintype tm] [DecidableEq tm][DecidableEq tn] [Fintype tn] (A : Matrix ( tm) ( tn) R) (i j :  tm) (x : R) (hij : i ≠ j) : Matrix ( tm) ( tn) R :=
  fun (r :  tm) => if r = j then x • A i + A j else A r

def row_update_by_eleRowAdd [Field R] {m n : ℕ } (A : Matrix (Fin m) (Fin n) R) (i : Fin m ) (ti : Fin m) (hi': ti < i) (k : Fin n) : Matrix (Fin m) (Fin n) R :=
  if h1: i < m then
    let A' := elementary_row_addition A (j := i) (i := ti) (hij := ne_of_lt hi') (x := - A i k / A ti k )

    if h2: i + 1 < m then
      let isucc := (Fin.mk (i+1) (h2))
      have hi'' : ti < isucc := by
        unfold isucc
        apply lt_trans hi'
        apply Fin.lt_succ
      row_update_by_eleRowAdd A' isucc (ti := ti) (hi' :=hi'' ) (k := k)

    else A'
  else A
def elimination_loop   [Inhabited R] {m n : ℕ } (A : Matrix (Fin m) (Fin n) R) (h : Fin m) (k: Fin n ) : Matrix (Fin m) (Fin n) R :=
  if  h <  m && k < n then
      /- Find the k-th pivot -/
      let i_max : Option (Fin m):= row_index_col_max_abs_arg A h k-- argmax (i = h ... m,abs (A [i,k]))
      match i_max with
      | none => panic "no pivot" -- panic 加Inhabited
      | some i_max' =>
      /-no pivot in this column, pass to the next column-/
        if A i_max' k = 0 then

          if hk : k + 1 < n then elimination_loop (A) (h) (Fin.mk (k + 1) (hk)) -- k' + 1
          else A
        else

          let A' := elementary_row_switch A h i_max'

          if h1: h +1 < m then
            let hsucc := (Fin.mk (h+1) (h1))
            /-+ （- A i k / A h k） * A h-/
            let A'' :=row_update_by_eleRowAdd A' hsucc (h) (hi':= by {unfold hsucc;apply Fin.lt_succ}) (k := k)
            if hk : k + 1 < n then
              elimination_loop (A'') (hsucc) (Fin.mk (k + 1) (hk)) -- k' + 1
            else A''
          else A'
  else A
def Gaussian_elimination   [Inhabited R] {m n : ℕ } (hm : m > 0) (hn : n > 0) (A : Matrix (Fin m) (Fin n) R): Matrix (Fin m) (Fin n) R :=
  let h : Fin m := Fin.mk (0) hm /-Initialization of the pivot row-/
  let k : Fin n:= Fin.mk (0) hn /-Initialization of the pivot column -/
  elimination_loop A h k

def row_echelon_form_from_Gaussian_eli  [Inhabited R] {m n : ℕ } (hm : m > 0) (hn : n > 0) (A : Matrix (Fin m) (Fin n) R): Matrix (Fin m) (Fin n) R := Gaussian_elimination hm hn A
def isRowEchelonForm {m n : ℕ }  (A : Matrix (Fin m) (Fin n) R): Prop :=
  ∃ f : Fin m → ℕ ,
   (∀ i j, A i j ≠ (0 : R) → f i ≤ j.val)
   ∧
   (∀ i : Fin m,(h : i.val < m -1) → f i < f (Fin.mk (i + 1) (Nat.succ_lt_of_lt_pred h)) ∨ f i = n)
/-I want to use Lean to prove that the execution result of Gaussian elimination is a RowEchelonForm matrix. Is this possible?-/
lemma rowEchelonFormOfGaussJordanEli_isRowEchelonForm {m n : ℕ }[ Inhabited R]  (hm : m>0) (hn : n > 0)(A : Matrix (Fin m) (Fin n) R):
  isRowEchelonForm (row_echelon_form_from_Gaussian_eli hm hn A) :=
    sorry