dsimp [get, set, Fin.cast, Fin.lexFold]
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j : Fin c
v : α
⊢ get (set a i j v) i j = v
α : Type u
r c : Nat
a : Matrix α r c
i : Fin r
j : Fin c
v : α
⊢ (Array.set a.entry
        { val := ↑i * c + ↑j,
          isLt := (_ : ↑{ val := ↑i * c + ↑j, isLt := (_ : ↑i * c + ↑j < r * c) } < Array.size a.entry) }
        v)[↑i * c + ↑j] =
    v