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

State before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
if h : i = j then
  subst j
  simp
else
  simp [h]
State after:
no goals

State before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
h : i = j
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
subst j
State after:
α : Type
n i : Nat
a : α
v : Vec α n
h₁ h₂ : i < n
⊢ (v.set i h₁ a)[i] = if i = i then a else v[i]

State before:
α : Type
n i : Nat
a : α
v : Vec α n
h₁ h₂ : i < n
⊢ (v.set i h₁ a)[i] = if i = i then a else v[i]
Tactic:
simp
State after:
no goals

State before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
h : ¬i = j
⊢ (v.set i h₁ a)[j] = if i = j then a else v[j]
Tactic:
simp [h]
State after:
no goals