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

State before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ (as ++ bs)[i] = as[i]
Tactic:
rewrite [getElem_eq_data_get]
State after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = as[i]

State before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = as[i]
Tactic:
rewrite [List.get_of_eq (Array.append_data as bs)]
State after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    as[i]

State before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    as[i]
Tactic:
rewrite [List.get_append_left as.data bs.data h]
State after:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get as.data { val := i, isLt := h } = as[i]

State before:
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get as.data { val := i, isLt := h } = as[i]
Tactic:
rfl
State after:
no goals