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

State before:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size as
⊢ (pop as)[i] = as[i]
Tactic:
simp only [pop, getElem_eq_data_get, List.dropLast_eq_take]
State after:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size 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 := hi₂ }

State before:
α : Type u
as : Array α
i : Nat
hi₁ : i < size (pop as)
hi₂ : i < size 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 := hi₂ }
Tactic:
exact as.data.get_take _ i
State after:
no goals