Theorem: get'_map (Saturn/Vector.lean)

State before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ get' (map f vec) j jw = f (get' vec j jw)
Tactic:
rw [get']
State after:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ Vector.get (map f vec) { val := j, isLt := jw } = f (get' vec j jw)

State before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ Vector.get (map f vec) { val := j, isLt := jw } = f (get' vec j jw)
Tactic:
simp [Vector.get_map]
State after:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ f (Vector.get vec { val := j, isLt := jw }) = f (get' vec j jw)

State before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ f (Vector.get vec { val := j, isLt := jw }) = f (get' vec j jw)
Tactic:
rfl
State after:
no goals