case nil
α : Type u_1
β : Type ?u.49282
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l)
n : ℕ
hn : n < length (tails [])
⊢ nthLe (tails []) n hn = drop n []

case cons
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n : ℕ
hn : n < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) n hn = drop n (x :: l)
α : Type u_1
β : Type ?u.49282
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l : List α
n : ℕ
hn : n < length (tails l)
⊢ nthLe (tails l) n hn = drop n l
induction' l with x l IH generalizing n
no goals
case nil
α : Type u_1
β : Type ?u.49282
l✝ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l)
n : ℕ
hn : n < length (tails [])
⊢ nthLe (tails []) n hn = drop n []
simp
case cons.zero
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
hn : zero < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) zero hn = drop zero (x :: l)

case cons.succ
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n✝ : ℕ
hn : succ n✝ < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) (succ n✝) hn = drop (succ n✝) (x :: l)
case cons
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n✝ : ℕ
hn✝ : n✝ < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n : ℕ
hn : n < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) n hn = drop n (x :: l)
cases n
no goals
case cons.zero
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
hn : zero < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) zero hn = drop zero (x :: l)
simp[nthLe_cons]
no goals
case cons.succ
α : Type u_1
β : Type ?u.49282
l✝¹ l₁ l₂ l₃ : List α
a b : α
m n✝¹ : ℕ
l✝ : List α
n : ℕ
hn✝ : n < length (tails l✝)
x : α
l : List α
IH : ∀ (n : ℕ) (hn : n < length (tails l)), nthLe (tails l) n hn = drop n l
n✝ : ℕ
hn : succ n✝ < length (tails (x :: l))
⊢ nthLe (tails (x :: l)) (succ n✝) hn = drop (succ n✝) (x :: l)
simpa[nthLe_cons] using IH _ _