Theorem: Array.getElem_swap (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
Tactic:
have : ∀ {m n : Nat} (h : m = n) (i : Fin m), ((h ▸ i) : Fin n).val = i.val :=
  @fun
  | _, _, rfl, _ => rfl
State after:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
this : ∀ {m n : Nat} (h : m = n) (i : Fin m), (h ▸ i).val = i.val
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]

State before:
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
this : ∀ {m n : Nat} (h : m = n) (i : Fin m), (h ▸ i).val = i.val
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
Tactic:
simp [swap, getElem_eq_data_get, List.get_set, this]
State after:
no goals