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

State before:
α : Type u
x : Array α
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] at hk ⊢
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
conv at hk => rewrite [Array.size_set]
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rewrite [(x.set i x[j.1]).get_set _ k hk]
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑((_ : size x = size (set x i (get x j))) ▸ j) = k then x[↑i] else (set x i x[↑j])[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑((_ : size x = size (set x i (get x j))) ▸ j) = k then x[↑i] else (set x i x[↑j])[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
simp only [← Fin.cast_eq_subst _ j, Fin.coe_cast]
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
conv at hk => rewrite [Array.size_set]
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝¹ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk✝ : k < size (set x i x[↑j])
hk : k < size x
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝¹ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk✝ : k < size (set x i x[↑j])
hk : k < size x
⊢ (if ↑j = k then x[↑i] else (set x i x[↑j])[k]) = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rw [x.get_set i k hk]
State after:
no goals