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