Theorem: Regex.Data.Vec.get_set_eq (Regex/Data/Vec/Basic.lean)

State before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ (v.set i h a)[i] = a
Tactic:
simp [Vec.set, getElem]
State after:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ i h = a

State before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ i h = a
Tactic:
unfold Vec.get
State after:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[i] = a

State before:
α : Type
n i : Nat
a : α
v : Vec α n
h : i < n
⊢ ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩.val[i] = a
Tactic:
simp
State after:
no goals