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

State before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ (pop as)[i] = as[i]
Tactic:
dsimp [pop]
State after:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ { data := List.dropLast as.data }[i] = as[i]

State before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ { data := List.dropLast as.data }[i] = as[i]
Tactic:
simp only [getElem_eq_data_get, List.dropLast_eq_take, List.get_take]
State after:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := (_ : i < size as) }

State before:
α : Type u
as : Array α
i : Nat
hi : i < size (pop as)
⊢ List.get (List.take (List.length as.data - 1) as.data)
      { val := i, isLt := (_ : (fun xs i => i < size xs) { data := List.take (List.length as.data - 1) as.data } i) } =
    List.get as.data { val := i, isLt := (_ : i < size as) }
Tactic:
exact as.data.get_take _ i
State after:
no goals