internlm/Lean-Github huggingface dataset:
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ { min := fun x y => if x ≤ y then x else y }.1 n m = n
Tactic:
simp only [ite_eq_left_iff, not_le]
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ m < n → m = n
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
⊢ m < n → m = n
Tactic:
intro hless
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hless : m < n
⊢ m = n
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : n ≤ m
x : α
xs : List α
hless : m < n
⊢ m = n
Tactic:
linarith
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Tactic:
rw [nat_succ_le_succ_iff] at h
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) xs) = take (succ m) xs
Tactic:
cases xs with
| nil =>
  rw [take]
  apply list_take_nil
| cons x xs =>
  repeat rw [take]
  apply (congrArg (cons x))
  have hmin : min n m = m := by
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only [ite_eq_right_iff]
    intro hless
    linarith
  have ihn' : _ := @ihn m xs
  rw [hmin] at ihn'
  exact ihn'
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) (take (succ m) []) = take (succ m) []
Tactic:
rw [take]
Proof state after:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) [] = []
Theorem: list_take_take
Proof state before:
case nil
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
⊢ take (succ n) [] = []
Tactic:
apply list_take_nil
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take (succ n) (take (succ m) (x :: xs)) = take (succ m) (x :: xs)
Tactic:
repeat rw [take]
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs
Tactic:
apply (congrArg (cons x))
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take m xs
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take n (take m xs) = take m xs
Tactic:
have hmin : min n m = m := by
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [ite_eq_right_iff]
  intro hless
  linarith
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
⊢ take n (take m xs) = take m xs
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
⊢ take n (take m xs) = take m xs
Tactic:
have ihn' : _ := @ihn m xs
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take m xs
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take m xs
Tactic:
rw [hmin] at ihn'
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take m xs
⊢ take n (take m xs) = take m xs
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hmin : min n m = m
ihn' : take n (take m xs) = take m xs
⊢ take n (take m xs) = take m xs
Tactic:
exact ihn'
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ take (succ n) (x :: take m xs) = x :: take m xs
Tactic:
rw [take]
Proof state after:
case cons
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ x :: take n (take m xs) = x :: take m xs
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ min n m = m
Tactic:
unfold min
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = m
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ instMinNat.1 n m = m
Tactic:
unfold instMinNat
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ minOfLe.1 n m = m
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ minOfLe.1 n m = m
Tactic:
unfold minOfLe
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ { min := fun x y => if x ≤ y then x else y }.1 n m = m
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ { min := fun x y => if x ≤ y then x else y }.1 n m = m
Tactic:
simp only [ite_eq_right_iff]
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ n ≤ m → n = m
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
⊢ n ≤ m → n = m
Tactic:
intro hless
Proof state after:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hless : n ≤ m
⊢ n = m
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
h : ¬n ≤ m
x : α
xs : List α
hless : n ≤ m
⊢ n = m
Tactic:
linarith
Proof state after:
no goals
Theorem: list_drop_O
Proof state before:
α : Type u_1
xs : List α
⊢ drop 0 xs = xs
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_zero
Proof state before:
α : Type u_1
xs : List α
⊢ drop zero xs = xs
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_nil
Proof state before:
α : Type u
n : ℕ
⊢ drop n [] = []
Tactic:
cases n with
| zero => rw [drop]
| succ n' => rw [drop]
Proof state after:
no goals
Theorem: list_drop_nil
Proof state before:
case zero
α : Type u
⊢ drop zero [] = []
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_nil
Proof state before:
case succ
α : Type u
n' : ℕ
⊢ drop (succ n') [] = []
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
α : Type u_1
n m : ℕ
xs : List α
⊢ take m (drop n xs) = drop n (take (n + m) xs)
Tactic:
revert m xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
Theorem: list_take_drop_comm
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
Tactic:
induction n with
| zero =>
  intro m xs
  rw [Nat.zero_add]
  repeat rw [list_drop_zero]
| succ n ih =>
  intro m xs
  cases xs with
  | nil =>
    rw [list_drop_nil, list_take_nil, list_take_nil, list_drop_nil]
  | cons x xs =>
    rw [drop]
    rw [nat_add_succ_is_succ_add]
    rw [take]
    rw [drop]
    apply ih
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
case zero
α : Type u_1
⊢ ∀ (m : ℕ) (xs : List α), take m (drop zero xs) = drop zero (take (zero + m) xs)
Tactic:
intro m xs
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take (zero + m) xs)
Theorem: list_take_drop_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take (zero + m) xs)
Tactic:
rw [Nat.zero_add]
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take m xs)
Theorem: list_take_drop_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take m xs)
Tactic:
repeat rw [list_drop_zero]
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m xs = drop zero (take m xs)
Tactic:
rw [list_drop_zero]
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
⊢ ∀ (m : ℕ) (xs : List α), take m (drop (succ n) xs) = drop (succ n) (take (succ n + m) xs)
Tactic:
intro m xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
xs : List α
⊢ take m (drop (succ n) xs) = drop (succ n) (take (succ n + m) xs)
Theorem: list_take_drop_comm
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
xs : List α
⊢ take m (drop (succ n) xs) = drop (succ n) (take (succ n + m) xs)
Tactic:
cases xs with
| nil =>
  rw [list_drop_nil, list_take_nil, list_take_nil, list_drop_nil]
| cons x xs =>
  rw [drop]
  rw [nat_add_succ_is_succ_add]
  rw [take]
  rw [drop]
  apply ih
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
⊢ take m (drop (succ n) []) = drop (succ n) (take (succ n + m) [])
Tactic:
rw [list_drop_nil, list_take_nil, list_take_nil, list_drop_nil]
Proof state after:
no goals
Theorem: list_take_drop_comm
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop (succ n) (x :: xs)) = drop (succ n) (take (succ n + m) (x :: xs))
Tactic:
rw [drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (take (succ n + m) (x :: xs))
Theorem: list_take_drop_comm
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (take (succ n + m) (x :: xs))
Tactic:
rw [nat_add_succ_is_succ_add]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (take (succ (n + m)) (x :: xs))
Theorem: list_take_drop_comm
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (take (succ (n + m)) (x :: xs))
Tactic:
rw [take]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (x :: take (n + m) xs)
Theorem: list_take_drop_comm
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop (succ n) (x :: take (n + m) xs)
Tactic:
rw [drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop n (take (n + m) xs)
Theorem: list_take_drop_comm
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
m : ℕ
x : α
xs : List α
⊢ take m (drop n xs) = drop n (take (n + m) xs)
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
α : Type u_1
n m : ℕ
xs : List α
⊢ drop m (take n xs) = take (n - m) (drop m xs)
Tactic:
revert m xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
Theorem: list_drop_take_comm
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
Tactic:
induction n with
| zero =>
  intro m xs
  rw [Nat.zero_sub]
  repeat rw [list_take_zero]
  rw [list_drop_nil]
| succ n ih =>
  intro m xs
  cases m with
  | zero =>
    rw [Nat.sub_zero]
    repeat rw [list_drop_zero]
  | succ m =>
    cases xs with
    | nil =>
      rw [list_take_nil, list_drop_nil, list_take_nil]
    | cons x xs =>
      rw [take]
      rw [drop]
      rw [Nat.succ_sub_succ]
      rw [drop]
      apply ih
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case zero
α : Type u_1
⊢ ∀ (m : ℕ) (xs : List α), drop m (take zero xs) = take (zero - m) (drop m xs)
Tactic:
intro m xs
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m (take zero xs) = take (zero - m) (drop m xs)
Theorem: list_drop_take_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m (take zero xs) = take (zero - m) (drop m xs)
Tactic:
rw [Nat.zero_sub]
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m (take zero xs) = take 0 (drop m xs)
Theorem: list_drop_take_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m (take zero xs) = take 0 (drop m xs)
Tactic:
repeat rw [list_take_zero]
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m [] = []
Theorem: list_drop_take_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m [] = []
Tactic:
rw [list_drop_nil]
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m [] = take 0 (drop m xs)
Tactic:
rw [list_take_zero]
Proof state after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ drop m [] = []
Theorem: list_drop_take_comm
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
⊢ ∀ (m : ℕ) (xs : List α), drop m (take (succ n) xs) = take (succ n - m) (drop m xs)
Tactic:
intro m xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
xs : List α
⊢ drop m (take (succ n) xs) = take (succ n - m) (drop m xs)
Theorem: list_drop_take_comm
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
xs : List α
⊢ drop m (take (succ n) xs) = take (succ n - m) (drop m xs)
Tactic:
cases m with
| zero =>
  rw [Nat.sub_zero]
  repeat rw [list_drop_zero]
| succ m =>
  cases xs with
  | nil =>
    rw [list_take_nil, list_drop_nil, list_take_nil]
  | cons x xs =>
    rw [take]
    rw [drop]
    rw [Nat.succ_sub_succ]
    rw [drop]
    apply ih
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case succ.zero
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
⊢ drop zero (take (succ n) xs) = take (succ n - zero) (drop zero xs)
Tactic:
rw [Nat.sub_zero]
Proof state after:
case succ.zero
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
⊢ drop zero (take (succ n) xs) = take (succ n) (drop zero xs)
Theorem: list_drop_take_comm
Proof state before:
case succ.zero
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
⊢ drop zero (take (succ n) xs) = take (succ n) (drop zero xs)
Tactic:
repeat rw [list_drop_zero]
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case succ.zero
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
⊢ take (succ n) xs = take (succ n) (drop zero xs)
Tactic:
rw [list_drop_zero]
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case succ.succ
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
m : ℕ
⊢ drop (succ m) (take (succ n) xs) = take (succ n - succ m) (drop (succ m) xs)
Tactic:
cases xs with
| nil =>
  rw [list_take_nil, list_drop_nil, list_take_nil]
| cons x xs =>
  rw [take]
  rw [drop]
  rw [Nat.succ_sub_succ]
  rw [drop]
  apply ih
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.nil
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
⊢ drop (succ m) (take (succ n) []) = take (succ n - succ m) (drop (succ m) [])
Tactic:
rw [list_take_nil, list_drop_nil, list_take_nil]
Proof state after:
no goals
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop (succ m) (take (succ n) (x :: xs)) = take (succ n - succ m) (drop (succ m) (x :: xs))
Tactic:
rw [take]
Proof state after:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop (succ m) (x :: take n xs) = take (succ n - succ m) (drop (succ m) (x :: xs))
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop (succ m) (x :: take n xs) = take (succ n - succ m) (drop (succ m) (x :: xs))
Tactic:
rw [drop]
Proof state after:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (succ n - succ m) (drop (succ m) (x :: xs))
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (succ n - succ m) (drop (succ m) (x :: xs))
Tactic:
rw [Nat.succ_sub_succ]
Proof state after:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (n - m) (drop (succ m) (x :: xs))
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (n - m) (drop (succ m) (x :: xs))
Tactic:
rw [drop]
Proof state after:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (n - m) (drop m xs)
Theorem: list_drop_take_comm
Proof state before:
case succ.succ.cons
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
m : ℕ
x : α
xs : List α
⊢ drop m (take n xs) = take (n - m) (drop m xs)
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_drop_cons
Proof state before:
α : Type u_1
n : ℕ
x : α
xs : List α
⊢ drop (n + 1) (x :: xs) = drop n xs
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_all
Proof state before:
α : Type u_1
xs : List α
⊢ drop (length xs) xs = []
Tactic:
induction xs with
| nil =>
  rw [list_drop_nil]
| cons head tail ih =>
  rw [length]
  rw [drop]
  exact ih
Proof state after:
no goals
Theorem: list_drop_all
Proof state before:
case nil
α : Type u_1
⊢ drop (length []) [] = []
Tactic:
rw [list_drop_nil]
Proof state after:
no goals
Theorem: list_drop_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length (head :: tail)) (head :: tail) = []
Tactic:
rw [length]
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail + 1) (head :: tail) = []
Theorem: list_drop_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail + 1) (head :: tail) = []
Tactic:
rw [drop]
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail) tail = []
Theorem: list_drop_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail) tail = []
Tactic:
exact ih
Proof state after:
no goals
Theorem: list_drop_all2
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length xs ≤ n → drop n xs = []
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → drop n xs = []
Theorem: list_drop_all2
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → drop n xs = []
Tactic:
induction n with
| zero =>
  intro xs
  intro h
  have empty_list := list_length_zero_or_smaller_is_empty xs h
  rw [empty_list]
  rw [drop]
| succ n ih =>
  intro xs
  cases xs with
  | nil =>
    rw [length]
    intro _
    rw [drop]
  | cons x xs =>
    rw [length]
    intro h
    rw [drop]
    rw [nat_succ_le_succ_iff] at h
    exact ih xs h
Proof state after:
no goals
Theorem: list_drop_all2
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), length xs ≤ zero → drop zero xs = []
Tactic:
intro xs
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ length xs ≤ zero → drop zero xs = []
Theorem: list_drop_all2
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ length xs ≤ zero → drop zero xs = []
Tactic:
intro h
Proof state after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ drop zero xs = []
Theorem: list_drop_all2
Proof state before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ drop zero xs = []
Tactic:
have empty_list := list_length_zero_or_smaller_is_empty xs h
Proof state after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero xs = []