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

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑i] = x[↑j]
Tactic:
rcases i with ⟨i,hi⟩
State after:
case mk
α : Type u
x : Subarray α
j : Fin (size x)
i : Nat
hi : i < size x
⊢ (swap x { val := i, isLt := hi } j)[↑{ val := i, isLt := hi }] = x[↑j]

State before:
case mk
α : Type u
x : Subarray α
j : Fin (size x)
i : Nat
hi : i < size x
⊢ (swap x { val := i, isLt := hi } j)[↑{ val := i, isLt := hi }] = x[↑j]
Tactic:
rcases j with ⟨j,hj⟩
State after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (swap x { val := i, isLt := hi } { val := j, isLt := hj })[↑{ val := i, isLt := hi }] = x[↑{ val := j, isLt := hj }]

State before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (swap x { val := i, isLt := hi } { val := j, isLt := hj })[↑{ val := i, isLt := hi }] = x[↑{ val := j, isLt := hj }]
Tactic:
rewrite [getElem_swap]
State after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if ↑{ val := j, isLt := hj } = ↑{ val := i, isLt := hi } then x[↑{ val := i, isLt := hi }]
    else
      if ↑{ val := i, isLt := hi } = ↑{ val := i, isLt := hi } then x[↑{ val := j, isLt := hj }]
      else x[↑{ val := i, isLt := hi }]) =
    x[↑{ val := j, isLt := hj }]

State before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if ↑{ val := j, isLt := hj } = ↑{ val := i, isLt := hi } then x[↑{ val := i, isLt := hi }]
    else
      if ↑{ val := i, isLt := hi } = ↑{ val := i, isLt := hi } then x[↑{ val := j, isLt := hj }]
      else x[↑{ val := i, isLt := hi }]) =
    x[↑{ val := j, isLt := hj }]
Tactic:
dsimp at *
State after:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]

State before:
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
if hji : j = i then
  cases hji; simp only [ite_true]
else
  rw [if_neg hji, if_pos rfl]
State after:
no goals

State before:
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
hji : j = i
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
cases hji
State after:
case refl
α : Type u
x : Subarray α
i : Nat
hi hj : i < size x
⊢ (if i = i then x[i] else if i = i then x[i] else x[i]) = x[i]

State before:
case refl
α : Type u
x : Subarray α
i : Nat
hi hj : i < size x
⊢ (if i = i then x[i] else if i = i then x[i] else x[i]) = x[i]
Tactic:
simp only [ite_true]
State after:
no goals

State before:
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
hji : ¬j = i
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
Tactic:
rw [if_neg hji, if_pos rfl]
State after:
no goals