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

State before:
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.set i h a).set i h b = v.set i h b
Tactic:
apply Subtype.eq
State after:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ ((v.set i h a).set i h b).val = (v.set i h b).val

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

State before:
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.val.set ⟨i, ⋯⟩ a).set ⟨i, ⋯⟩ b = v.val.set ⟨i, ⋯⟩ b
Tactic:
rw [Array.set_set]
State after:
no goals