case zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n m✝ : ℕ
h✝ : m✝ < n
l : List α
m : ℕ
h : m < zero
⊢ get? (take zero l) m = get? l m

case succ
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
l : List α
m : ℕ
h : m < succ n
⊢ get? (take (succ n) l) m = get? l m
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n m : ℕ
h : m < n
⊢ get? (take n l) m = get? l m
induction' n with n hn generalizing l m
case zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n m✝ : ℕ
h✝ : m✝ < n
l : List α
m : ℕ
h : m < 0
⊢ get? (take zero l) m = get? l m
case zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n m✝ : ℕ
h✝ : m✝ < n
l : List α
m : ℕ
h : m < zero
⊢ get? (take zero l) m = get? l m
simp only [Nat.zero_eq] at h
no goals
case zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n m✝ : ℕ
h✝ : m✝ < n
l : List α
m : ℕ
h : m < 0
⊢ get? (take zero l) m = get? l m
exact absurd h (not_lt_of_le m.zero_le)
case succ.nil
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
m : ℕ
h : m < succ n
⊢ get? (take (succ n) []) m = get? [] m

case succ.cons
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
m : ℕ
h : m < succ n
hd : α
tl : List α
⊢ get? (take (succ n) (hd :: tl)) m = get? (hd :: tl) m
case succ
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
l : List α
m : ℕ
h : m < succ n
⊢ get? (take (succ n) l) m = get? l m
cases' l with hd tl
no goals
case succ.nil
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
m : ℕ
h : m < succ n
⊢ get? (take (succ n) []) m = get? [] m
simp only [take_nil]
case succ.cons.zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m : ℕ
h✝ : m < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
hd : α
tl : List α
h : zero < succ n
⊢ get? (take (succ n) (hd :: tl)) zero = get? (hd :: tl) zero

case succ.cons.succ
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝¹ m : ℕ
h✝ : m < n✝¹
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
hd : α
tl : List α
n✝ : ℕ
h : succ n✝ < succ n
⊢ get? (take (succ n) (hd :: tl)) (succ n✝) = get? (hd :: tl) (succ n✝)
case succ.cons
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m✝ : ℕ
h✝ : m✝ < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
m : ℕ
h : m < succ n
hd : α
tl : List α
⊢ get? (take (succ n) (hd :: tl)) m = get? (hd :: tl) m
cases m
no goals
case succ.cons.zero
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝ m : ℕ
h✝ : m < n✝
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
hd : α
tl : List α
h : zero < succ n
⊢ get? (take (succ n) (hd :: tl)) zero = get? (hd :: tl) zero
simp only [get?, take]
no goals
case succ.cons.succ
ι : Type ?u.170021
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n✝¹ m : ℕ
h✝ : m < n✝¹
n : ℕ
hn : ∀ {l : List α} {m : ℕ}, m < n → get? (take n l) m = get? l m
hd : α
tl : List α
n✝ : ℕ
h : succ n✝ < succ n
⊢ get? (take (succ n) (hd :: tl)) (succ n✝) = get? (hd :: tl) (succ n✝)
simpa only using hn (Nat.lt_of_succ_lt_succ h)