Theorem: List.extract_step (Extra/List.lean)

State before:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ as.extract start stop = as.get ⟨start, ⋯⟩ :: as.extract (start + 1) stop
Tactic:
unfold extract
State after:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)

State before:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Tactic:
induction start, stop using Nat.recDiag generalizing as with
| zero_zero => contradiction
| succ_zero start => contradiction
| zero_succ stop => match as with | a :: as => simp
| succ_succ start stop ih =>
  match as with
  | a :: as =>
    simp
    rw [ih]
    exact Nat.lt_of_succ_lt_succ hstart
    exact Nat.le_of_succ_le_succ hstop
State after:
no goals

State before:
case zero_zero
α : Type u_1
as : List α
hstart : 0 < 0
hstop : 0 ≤ as.length
⊢ take (0 - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (0 - (0 + 1)) (drop (0 + 1) as)
Tactic:
contradiction
State after:
no goals

State before:
case succ_zero
α : Type u_1
start : Nat
a✝ :
  ∀ (as : List α) (hstart : start < 0) (hstop : 0 ≤ as.length),
    take (0 - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (0 - (start + 1)) (drop (start + 1) as)
as : List α
hstart : start + 1 < 0
hstop : 0 ≤ as.length
⊢ take (0 - (start + 1)) (drop (start + 1) as) =
    as.get ⟨start + 1, ⋯⟩ :: take (0 - (start + 1 + 1)) (drop (start + 1 + 1) as)
Tactic:
contradiction
State after:
no goals

State before:
case zero_succ
α : Type u_1
stop : Nat
a✝ :
  ∀ (as : List α) (hstart : 0 < stop) (hstop : stop ≤ as.length),
    take (stop - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop - (0 + 1)) (drop (0 + 1) as)
as : List α
hstart : 0 < stop + 1
hstop : stop + 1 ≤ as.length
⊢ take (stop + 1 - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop + 1 - (0 + 1)) (drop (0 + 1) as)
Tactic:
match as with | a :: as => simp
State after:
no goals

State before:
α : Type u_1
stop : Nat
a✝ :
  ∀ (as : List α) (hstart : 0 < stop) (hstop : stop ≤ as.length),
    take (stop - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop - (0 + 1)) (drop (0 + 1) as)
as✝ : List α
hstart : 0 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop + 1 - 0) (drop 0 (a :: as)) = (a :: as).get ⟨0, ⋯⟩ :: take (stop + 1 - (0 + 1)) (drop (0 + 1) (a :: as))
Tactic:
simp
State after:
no goals

State before:
case succ_succ
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as : List α
hstart : start + 1 < stop + 1
hstop : stop + 1 ≤ as.length
⊢ take (stop + 1 - (start + 1)) (drop (start + 1) as) =
    as.get ⟨start + 1, ⋯⟩ :: take (stop + 1 - (start + 1 + 1)) (drop (start + 1 + 1) as)
Tactic:
match as with
| a :: as =>
  simp
  rw [ih]
  exact Nat.lt_of_succ_lt_succ hstart
  exact Nat.le_of_succ_le_succ hstop
State after:
no goals

State before:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop + 1 - (start + 1)) (drop (start + 1) (a :: as)) =
    (a :: as).get ⟨start + 1, ⋯⟩ :: take (stop + 1 - (start + 1 + 1)) (drop (start + 1 + 1) (a :: as))
Tactic:
simp
State after:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)

State before:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Tactic:
rw [ih]
State after:
case hstart
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ start < stop

case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length

State before:
case hstart
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ start < stop

case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Tactic:
exact Nat.lt_of_succ_lt_succ hstart
State after:
case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length

State before:
case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Tactic:
exact Nat.le_of_succ_le_succ hstop
State after:
no goals