Theorem: Matrix.get_set_eq (Algdata/Data/Matrix/Basic.lean)

State before:
α : 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
Tactic:
dsimp [get, set, Fin.cast, Fin.lexFold]
State after:
α : 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

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