Theorem: SizedArray.swap_comm (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ swap x i j = swap x j i
Tactic:
iterate rewrite [swap_eq]
State after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
if hij : i = j then
  cases hij; rfl
else
  exact x.set_set_comm hij x[j.1] x[i.1]
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = swap x j i
Tactic:
rewrite [swap_eq]
State after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
hij : i = j
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
cases hij
State after:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
⊢ set (set x i x[↑i]) i x[↑i] = set (set x i x[↑i]) i x[↑i]

State before:
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
⊢ set (set x i x[↑i]) i x[↑i] = set (set x i x[↑i]) i x[↑i]
Tactic:
rfl
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
hij : ¬i = j
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]
Tactic:
exact x.set_set_comm hij x[j.1] x[i.1]
State after:
no goals