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

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

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

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

State before:
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ (v.val.set ⟨i, ⋯⟩ a)[j] = v.val[j]
Tactic:
rw [Array.get_set_ne]
State after:
case h
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ↑⟨i, ⋯⟩ ≠ j

State before:
case h
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ ↑⟨i, ⋯⟩ ≠ j
Tactic:
assumption
State after:
no goals