case nil
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
n : ℕ
h : n < length []
⊢ take 1 (drop n []) = [get [] { val := n, isLt := h }]

case cons
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
h : n < length l
⊢ take 1 (drop n l) = [get l { val := n, isLt := h }]
induction' l with x l ih generalizing n
no goals
case nil
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
n : ℕ
h : n < length []
⊢ take 1 (drop n []) = [get [] { val := n, isLt := h }]
cases h
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : l = []
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]

case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
case cons
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
by_cases h₁ : l = []
case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
h₂ : n < length (x :: l)
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
have h₂ := h
case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
h₂ : n = length l ∨ n < length l
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
h₂ : n < length (x :: l)
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
rw [length_cons, Nat.lt_succ_iff, le_iff_eq_or_lt] at h₂
case neg.zero
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
h : zero < length (x :: l)
h₂ : zero = length l ∨ zero < length l
⊢ take 1 (drop zero (x :: l)) = [get (x :: l) { val := zero, isLt := h }]

case neg.succ
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
n✝ : ℕ
h : succ n✝ < length (x :: l)
h₂ : succ n✝ = length l ∨ succ n✝ < length l
⊢ take 1 (drop (succ n✝) (x :: l)) = [get (x :: l) { val := succ n✝, isLt := h }]
case neg
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : ¬l = []
h₂ : n = length l ∨ n < length l
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
cases n
case neg.succ
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
n✝ : ℕ
h : succ n✝ < length (x :: l)
h₂ : succ n✝ = length l ∨ succ n✝ < length l
⊢ take 1 (drop n✝ l) = [get l { val := n✝, isLt := (_ : succ n✝ ≤ length l) }]
case neg.succ
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
n✝ : ℕ
h : succ n✝ < length (x :: l)
h₂ : succ n✝ = length l ∨ succ n✝ < length l
⊢ take 1 (drop (succ n✝) (x :: l)) = [get (x :: l) { val := succ n✝, isLt := h }]
rw [drop, get]
no goals
case neg.succ
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
n✝ : ℕ
h : succ n✝ < length (x :: l)
h₂ : succ n✝ = length l ∨ succ n✝ < length l
⊢ take 1 (drop n✝ l) = [get l { val := n✝, isLt := (_ : succ n✝ ≤ length l) }]
apply ih
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n < length [x]
⊢ take 1 (drop n [x]) = [get [x] { val := n, isLt := h }]
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ : ℕ
h✝ : n✝ < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
n : ℕ
h : n < length (x :: l)
h₁ : l = []
⊢ take 1 (drop n (x :: l)) = [get (x :: l) { val := n, isLt := h }]
subst h₁
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n < length [x]
⊢ take 1 (drop n [x]) = [x]
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n < length [x]
⊢ take 1 (drop n [x]) = [get [x] { val := n, isLt := h }]
rw [get_singleton]
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n = 0
⊢ take 1 (drop n [x]) = [x]
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n < length [x]
⊢ take 1 (drop n [x]) = [x]
simp [lt_succ_iff] at h
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
h : n < length l
x : α
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
⊢ take 1 (drop 0 [x]) = [x]
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ : ℕ
h✝ : n✝ < length l
x : α
n : ℕ
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
h : n = 0
⊢ take 1 (drop n [x]) = [x]
subst h
no goals
case pos
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n : ℕ
h : n < length l
x : α
ih : ∀ {n : ℕ} (h : n < length []), take 1 (drop n []) = [get [] { val := n, isLt := h }]
⊢ take 1 (drop 0 [x]) = [x]
simp
no goals
case neg.zero
ι : Type ?u.89571
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n : ℕ
h✝ : n < length l✝
x : α
l : List α
ih : ∀ {n : ℕ} (h : n < length l), take 1 (drop n l) = [get l { val := n, isLt := h }]
h₁ : ¬l = []
h : zero < length (x :: l)
h₂ : zero = length l ∨ zero < length l
⊢ take 1 (drop zero (x :: l)) = [get (x :: l) { val := zero, isLt := h }]
simp [get]