no goals
α : Type u_1
i : Nat
as bs : List α
h : ¬i < length as
h' : i < length (as ++ bs)
h'' : i - length as < length bs
⊢ get (as ++ bs) { val := i, isLt := h' } = get bs { val := i - length as, isLt := h'' }
induction as generalizing i with
| nil => trivial
| cons a as ih =>
  cases i with simp [get, Nat.succ_sub_succ] <;> simp_arith [Nat.succ_sub_succ] at h
  | succ i => apply ih; simp_arith [h]
no goals
case nil
α : Type u_1
bs : List α
i : Nat
h : ¬i < length []
h' : i < length ([] ++ bs)
h'' : i - length [] < length bs
⊢ get ([] ++ bs) { val := i, isLt := h' } = get bs { val := i - length [], isLt := h'' }
trivial
no goals
case cons
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat},
    ¬i < length as →
      ∀ {h' : i < length (as ++ bs)} {h'' : i - length as < length bs},
        get (as ++ bs) { val := i, isLt := h' } = get bs { val := i - length as, isLt := h'' }
i : Nat
h : ¬i < length (a :: as)
h' : i < length (a :: as ++ bs)
h'' : i - length (a :: as) < length bs
⊢ get (a :: as ++ bs) { val := i, isLt := h' } = get bs { val := i - length (a :: as), isLt := h'' }
cases i with simp [get, Nat.succ_sub_succ] <;> simp_arith [Nat.succ_sub_succ] at h
| succ i => apply ih; simp_arith [h]
case cons.succ.h
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat},
    ¬i < length as →
      ∀ {h' : i < length (as ++ bs)} {h'' : i - length as < length bs},
        get (as ++ bs) { val := i, isLt := h' } = get bs { val := i - length as, isLt := h'' }
i : Nat
h' : Nat.succ i < length (a :: as ++ bs)
h'' : Nat.succ i - length (a :: as) < length bs
h : length as ≤ i
⊢ ¬i < length as
case cons.succ
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat},
    ¬i < length as →
      ∀ {h' : i < length (as ++ bs)} {h'' : i - length as < length bs},
        get (as ++ bs) { val := i, isLt := h' } = get bs { val := i - length as, isLt := h'' }
i : Nat
h' : Nat.succ i < length (a :: as ++ bs)
h'' : Nat.succ i - length (a :: as) < length bs
h : length as ≤ i
⊢ get (as ++ bs) { val := i, isLt := (_ : Nat.succ i ≤ length (List.append as bs)) } =
    get bs { val := i - length as, isLt := (_ : i - length as < length bs) }
apply ih
no goals
case cons.succ.h
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat},
    ¬i < length as →
      ∀ {h' : i < length (as ++ bs)} {h'' : i - length as < length bs},
        get (as ++ bs) { val := i, isLt := h' } = get bs { val := i - length as, isLt := h'' }
i : Nat
h' : Nat.succ i < length (a :: as ++ bs)
h'' : Nat.succ i - length (a :: as) < length bs
h : length as ≤ i
⊢ ¬i < length as
simp_arith [h]