no goals
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (length as)
⊢ sizeOf (get as i) < sizeOf as
match as, i with
| a::as, ⟨0, _⟩  => simp_arith [get]
| a::as, ⟨i+1, h⟩ =>
  have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
  apply Nat.lt_trans ih
  simp_arith
no goals
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i : Fin (length as✝)
a : α
as : List α
isLt✝ : 0 < length (a :: as)
⊢ sizeOf (get (a :: as) { val := 0, isLt := isLt✝ }) < sizeOf (a :: as)
simp_arith [get]
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h : i + 1 < length (a :: as)
ih : sizeOf (get as { val := i, isLt := (_ : Nat.succ i ≤ length as) }) < sizeOf as
⊢ sizeOf (get (a :: as) { val := i + 1, isLt := h }) < sizeOf (a :: as)
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h : i + 1 < length (a :: as)
⊢ sizeOf (get (a :: as) { val := i + 1, isLt := h }) < sizeOf (a :: as)
have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h : i + 1 < length (a :: as)
ih : sizeOf (get as { val := i, isLt := (_ : Nat.succ i ≤ length as) }) < sizeOf as
⊢ sizeOf as < sizeOf (a :: as)
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h : i + 1 < length (a :: as)
ih : sizeOf (get as { val := i, isLt := (_ : Nat.succ i ≤ length as) }) < sizeOf as
⊢ sizeOf (get (a :: as) { val := i + 1, isLt := h }) < sizeOf (a :: as)
apply Nat.lt_trans ih
no goals
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h : i + 1 < length (a :: as)
ih : sizeOf (get as { val := i, isLt := (_ : Nat.succ i ≤ length as) }) < sizeOf as
⊢ sizeOf as < sizeOf (a :: as)
simp_arith