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

State before:
α : Type u
as : Array α
i j : Fin (size as)
⊢ swap as i j = swap as j i
Tactic:
apply Array.ext'
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ (swap as i j).data = (swap as j i).data

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ (swap as i j).data = (swap as j i).data
Tactic:
simp only [Array.data_swap]
State after:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)

State before:
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
if h : i.1 = j.1 then
  cases Fin.eq_of_val_eq h; rfl
else
  rw [List.set_comm _ _ _ h]
State after:
no goals

State before:
α : Type u
as : Array α
i j : Fin (size as)
h : i.val = j.val
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
cases Fin.eq_of_val_eq h
State after:
case refl
α : Type u
as : Array α
i : Fin (size as)
h : i.val = i.val
⊢ List.set (List.set as.data i.val (get as i)) i.val (get as i) =
    List.set (List.set as.data i.val (get as i)) i.val (get as i)

State before:
case refl
α : Type u
as : Array α
i : Fin (size as)
h : i.val = i.val
⊢ List.set (List.set as.data i.val (get as i)) i.val (get as i) =
    List.set (List.set as.data i.val (get as i)) i.val (get as i)
Tactic:
rfl
State after:
no goals

State before:
α : Type u
as : Array α
i j : Fin (size as)
h : ¬i.val = j.val
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
Tactic:
rw [List.set_comm _ _ _ h]
State after:
no goals