Theorem: List.drop_get (GMLInit/Data/List/Basic.lean)

State before:
α : Type u_1
as : List α
n : Nat
hn : n < as.length
⊢ drop n as = as[n] :: drop (n + 1) as
Tactic:
induction as generalizing n with
| nil => absurd hn; exact Nat.not_lt_zero n
| cons a as ih =>
  match n with
  | 0 =>
    rw [drop_succ_cons]
    rw [drop]
    rw [getElem_eq_get]
    rw [get]
    rw [drop]
  | n+1 =>
    rw [drop_succ_cons]
    rw [drop_succ_cons]
    rw [getElem_eq_get]
    rw [get_cons_succ]
    rw [←getElem_eq_get]
    exact ih ..
State after:
no goals

State before:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ drop n [] = [][n] :: drop (n + 1) []
Tactic:
absurd hn
State after:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ ¬n < [].length

State before:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ ¬n < [].length
Tactic:
exact Nat.not_lt_zero n
State after:
no goals

State before:
case cons
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : n < (a :: as).length
⊢ drop n (a :: as) = (a :: as)[n] :: drop (n + 1) (a :: as)
Tactic:
match n with
| 0 =>
  rw [drop_succ_cons]
  rw [drop]
  rw [getElem_eq_get]
  rw [get]
  rw [drop]
| n+1 =>
  rw [drop_succ_cons]
  rw [drop_succ_cons]
  rw [getElem_eq_get]
  rw [get_cons_succ]
  rw [←getElem_eq_get]
  exact ih ..
State after:
no goals

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop (0 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop 0 as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop 0 as
Tactic:
rw [drop]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as)[0] :: drop 0 as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as)[0] :: drop 0 as
Tactic:
rw [getElem_eq_get]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as).get ⟨0, hn⟩ :: drop 0 as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as).get ⟨0, hn⟩ :: drop 0 as
Tactic:
rw [get]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = a :: drop 0 as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = a :: drop 0 as
Tactic:
rw [drop]
State after:
no goals

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop (n + 1) (a :: as) = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1) as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1) as
Tactic:
rw [getElem_eq_get]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as).get ⟨n + 1, hn⟩ :: drop (n + 1) as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as).get ⟨n + 1, hn⟩ :: drop (n + 1) as
Tactic:
rw [get_cons_succ]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as.get ⟨n, ⋯⟩ :: drop (n + 1) as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as.get ⟨n, ⋯⟩ :: drop (n + 1) as
Tactic:
rw [←getElem_eq_get]
State after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as[n] :: drop (n + 1) as

State before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as[n] :: drop (n + 1) as
Tactic:
exact ih ..
State after:
no goals