no goals
case nil
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
i j : ℕ
hj : 0 < j
hi : i < length []
⊢ sizeOf (dropSlice i j []) < sizeOf []
cases hi
case cons.zero
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
hi : zero < length (x :: xs)
⊢ sizeOf (drop j (x :: xs)) < sizeOf (x :: xs)

case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ sizeOf (x :: dropSlice n✝ j xs) < sizeOf (x :: xs)
case cons
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
i j : ℕ
hj : 0 < j
hi : i < length (x :: xs)
⊢ sizeOf (dropSlice i j (x :: xs)) < sizeOf (x :: xs)
cases i <;> simp only [List.dropSlice]
no goals
case cons.zero.zero
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
hj : 0 < zero
⊢ sizeOf (drop zero (x :: xs)) < sizeOf (x :: xs)
contradiction
case cons.zero.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop n xs) < sizeOf (x :: xs)
case cons.zero.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop (succ n) (x :: xs)) < sizeOf (x :: xs)
dsimp only [drop]
case cons.zero.succ.a
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop n xs) ≤ sizeOf xs

case cons.zero.succ.a
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf xs < sizeOf (x :: xs)
case cons.zero.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop n xs) < sizeOf (x :: xs)
apply @lt_of_le_of_lt _ _ _ (sizeOf xs)
no goals
case cons.zero.succ.a.nil
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length [] → sizeOf (dropSlice i j []) < sizeOf []
hi : zero < length [x]
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop n []) ≤ sizeOf []
rw [drop_nil]
case cons.zero.succ.a.cons.zero
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
hj : 0 < succ zero
⊢ sizeOf (drop zero (head✝ :: xs_tl)) ≤ sizeOf (head✝ :: xs_tl)

case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ sizeOf (drop (succ n✝) (head✝ :: xs_tl)) ≤ sizeOf (head✝ :: xs_tl)
case cons.zero.succ.a.cons
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n : ℕ
hj : 0 < succ n
⊢ sizeOf (drop n (head✝ :: xs_tl)) ≤ sizeOf (head✝ :: xs_tl)
cases n
no goals
case cons.zero.succ.a.cons.zero
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
hj : 0 < succ zero
⊢ sizeOf (drop zero (head✝ :: xs_tl)) ≤ sizeOf (head✝ :: xs_tl)
simp
case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ sizeOf (drop n✝ xs_tl) ≤ 1 + sizeOf head✝ + sizeOf xs_tl
case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ sizeOf (drop (succ n✝) (head✝ :: xs_tl)) ≤ sizeOf (head✝ :: xs_tl)
simp [drop]
case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ 0 + sizeOf (drop n✝ xs_tl) ≤ 1 + sizeOf head✝ + sizeOf xs_tl
case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ sizeOf (drop n✝ xs_tl) ≤ 1 + sizeOf head✝ + sizeOf xs_tl
rw [←Nat.zero_add (sizeOf (drop _ xs_tl))]
no goals
case cons.zero.succ.a.cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x head✝ : α
xs_tl : List α
tail_ih✝ :
  (∀ (i j : ℕ), 0 < j → i < length xs_tl → sizeOf (dropSlice i j xs_tl) < sizeOf xs_tl) →
    zero < length (x :: xs_tl) → ∀ (n : ℕ), 0 < succ n → sizeOf (drop n xs_tl) ≤ sizeOf xs_tl
xs_ih :
  ∀ (i j : ℕ), 0 < j → i < length (head✝ :: xs_tl) → sizeOf (dropSlice i j (head✝ :: xs_tl)) < sizeOf (head✝ :: xs_tl)
hi : zero < length (x :: head✝ :: xs_tl)
n✝ : ℕ
hj : 0 < succ (succ n✝)
⊢ 0 + sizeOf (drop n✝ xs_tl) ≤ 1 + sizeOf head✝ + sizeOf xs_tl
exact Nat.add_le_add (Nat.zero_le _) (drop_sizeOf_le xs_tl _)
no goals
case cons.zero.succ.a
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
hi : zero < length (x :: xs)
n : ℕ
hj : 0 < succ n
⊢ sizeOf xs < sizeOf (x :: xs)
simp
case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ sizeOf (dropSlice n✝ j xs) < sizeOf xs
case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ sizeOf (x :: dropSlice n✝ j xs) < sizeOf (x :: xs)
simp
case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ n✝ < length xs
case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ sizeOf (dropSlice n✝ j xs) < sizeOf xs
apply xs_ih _ j hj
no goals
case cons.succ
ι : Type ?u.498147
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), 0 < j → i < length xs → sizeOf (dropSlice i j xs) < sizeOf xs
j : ℕ
hj : 0 < j
n✝ : ℕ
hi : succ n✝ < length (x :: xs)
⊢ n✝ < length xs
apply lt_of_succ_lt_succ hi