Theorem: Subarray.getElem_swap (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (swap x i j)[k] = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
dsimp [swap, getElem]
State after:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ get
      { as := Array.swap x.as (castIndex x i) (castIndex x j), start := x.start, stop := x.stop,
        h₁ := (_ : x.start ≤ x.stop),
        h₂ := (_ : x.stop ≤ Array.size (Array.swap x.as (castIndex x i) (castIndex x j))) }
      { val := k, isLt := hk } =
    if ↑j = k then get x { val := ↑i, isLt := (_ : ↑i < size x) }
    else if ↑i = k then get x { val := ↑j, isLt := (_ : ↑j < size x) } else get x { val := k, isLt := hk }

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ get
      { as := Array.swap x.as (castIndex x i) (castIndex x j), start := x.start, stop := x.stop,
        h₁ := (_ : x.start ≤ x.stop),
        h₂ := (_ : x.stop ≤ Array.size (Array.swap x.as (castIndex x i) (castIndex x j))) }
      { val := k, isLt := hk } =
    if ↑j = k then get x { val := ↑i, isLt := (_ : ↑i < size x) }
    else if ↑i = k then get x { val := ↑j, isLt := (_ : ↑j < size x) } else get x { val := k, isLt := hk }
Tactic:
dsimp [get]
State after:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (Array.swap x.as (castIndex x i) (castIndex x j))[x.start + k] =
    if ↑j = k then x.as[x.start + ↑i] else if ↑i = k then x.as[x.start + ↑j] else x.as[x.start + k]

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (Array.swap x.as (castIndex x i) (castIndex x j))[x.start + k] =
    if ↑j = k then x.as[x.start + ↑i] else if ↑i = k then x.as[x.start + ↑j] else x.as[x.start + k]
Tactic:
simp only [Array.getElem_swap, castIndex, Nat.add_left_cancel_iff]
State after:
no goals