case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf (get { data := data✝ } i) < sizeOf { data := data✝ }
α : Type u_1
inst✝ : SizeOf α
as : Array α
i : Fin (size as)
⊢ sizeOf (get as i) < sizeOf as
cases as
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
⊢ sizeOf (get { data := as } i) < sizeOf { data := as }
case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf (get { data := data✝ } i) < sizeOf { data := data✝ }
rename_i as
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
⊢ sizeOf (List.get as i) < 1 + sizeOf as
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
⊢ sizeOf (get { data := as } i) < sizeOf { data := as }
simp [get]
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
ih : sizeOf (List.get as i) < sizeOf as
⊢ sizeOf (List.get as i) < 1 + sizeOf as
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
⊢ sizeOf (List.get as i) < 1 + sizeOf as
have ih := List.sizeOf_get_lt as i
no goals
case mk
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
ih : sizeOf (List.get as i) < sizeOf as
⊢ sizeOf (List.get as i) < 1 + sizeOf as
exact Nat.lt_trans ih (by simp_arith)
no goals
α : Type u_1
inst✝ : SizeOf α
as : List α
i : Fin (size { data := as })
ih : sizeOf (List.get as i) < sizeOf as
⊢ sizeOf as < 1 + sizeOf as
simp_arith