rw [Array.get_set_eq a.entry]
α : 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
no goals