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 α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf (List.get data✝ i) < 1 + sizeOf data✝
case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf (get { data := data✝ } i) < sizeOf { data := data✝ }
simp [get]
case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf data✝ < 1 + sizeOf data✝
case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf (List.get data✝ i) < 1 + sizeOf data✝
apply Nat.lt_trans (List.sizeOf_get ..)
no goals
case mk
α : Type u_1
inst✝ : SizeOf α
data✝ : List α
i : Fin (size { data := data✝ })
⊢ sizeOf data✝ < 1 + sizeOf data✝
simp_arith