no goals
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (length as)
⊢ sizeOf (get as i) < sizeOf as
match as, i with
| [],    i      => apply Fin.elim0 i
| a::as, ⟨0, _⟩ => simp_arith [get]
| a::as, ⟨i+1, h⟩ =>
  simp [get]
  have h : i < as.length := Nat.lt_of_succ_lt_succ h
  have ih := sizeOf_get_lt as ⟨i, h⟩
  exact Nat.lt_of_lt_of_le ih (Nat.le_add_left ..)
no goals
α : Type u_1
inst✝ : SizeOf α
as : List α
i✝ : Fin (length as)
i : Fin (length [])
⊢ sizeOf (get [] i) < sizeOf []
apply Fin.elim0 i
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)
⊢ sizeOf (get as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf 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)
simp [get]
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h✝ : i + 1 < length (a :: as)
h : i < length as
⊢ sizeOf (get as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf 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 as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf as
have h : i < as.length := Nat.lt_of_succ_lt_succ h
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h✝ : i + 1 < length (a :: as)
h : i < length as
ih : sizeOf (get as { val := i, isLt := h }) < sizeOf as
⊢ sizeOf (get as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf as
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h✝ : i + 1 < length (a :: as)
h : i < length as
⊢ sizeOf (get as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf as
have ih := sizeOf_get_lt as ⟨i, h⟩
no goals
α : Type u_1
inst✝ : SizeOf α
as✝ : List α
i✝ : Fin (length as✝)
a : α
as : List α
i : Nat
h✝ : i + 1 < length (a :: as)
h : i < length as
ih : sizeOf (get as { val := i, isLt := h }) < sizeOf as
⊢ sizeOf (get as { val := i, isLt := (_ : i < length as) }) < 1 + sizeOf a + sizeOf as
exact Nat.lt_of_lt_of_le ih (Nat.le_add_left ..)