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

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j).val = (set (set x i x[↑j]) j x[↑i]).val
Tactic:
dsimp only [swap]
State after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j) =
    (set (set x i x[↑j]) j x[↑i]).val

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j) =
    (set (set x i x[↑j]) j x[↑i]).val
Tactic:
simp only [Array.swap_def]
State after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.set
      (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
        (Array.get x.val (Fin.cast (_ : n = Array.size x.val) j)))
      { val := ↑(Fin.cast (_ : n = Array.size x.val) j),
        isLt :=
          (_ :
            ↑(Fin.cast (_ : n = Array.size x.val) j) <
              Array.size
                (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
                  x.val[↑(Fin.cast (_ : n = Array.size x.val) j)])) }
      (Array.get x.val (Fin.cast (_ : n = Array.size x.val) i)) =
    (set (set x i x[↑j]) j x[↑i]).val

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.set
      (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
        (Array.get x.val (Fin.cast (_ : n = Array.size x.val) j)))
      { val := ↑(Fin.cast (_ : n = Array.size x.val) j),
        isLt :=
          (_ :
            ↑(Fin.cast (_ : n = Array.size x.val) j) <
              Array.size
                (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
                  x.val[↑(Fin.cast (_ : n = Array.size x.val) j)])) }
      (Array.get x.val (Fin.cast (_ : n = Array.size x.val) i)) =
    (set (set x i x[↑j]) j x[↑i]).val
Tactic:
rfl
State after:
no goals