Theorem: Array.getElem_append_right (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] = bs[i - size as]
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' } = bs[i - size as]

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' } = bs[i - size as]
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)) } =
    bs[i - size as]

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)) } =
    bs[i - size as]
Tactic:
rewrite [List.get_append_right' h]
State after:
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get bs.data { val := i - List.length as.data, isLt := (_ : i - List.length as.data < List.length bs.data) } =
    bs[i - size as]

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