internlm/Lean-Github huggingface dataset:
Theorem: list_rev_eq
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
⊢ xs = ys
Tactic:
have h' : reverse (reverse xs) = reverse (reverse ys) :=
  congrArg reverse h
Proof state after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : reverse (reverse xs) = reverse (reverse ys)
⊢ xs = ys
Theorem: list_rev_eq
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : reverse (reverse xs) = reverse (reverse ys)
⊢ xs = ys
Tactic:
simp only [reverse_reverse] at h'
Proof state after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : xs = ys
⊢ xs = ys
Theorem: list_rev_eq
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : xs = ys
⊢ xs = ys
Tactic:
assumption
Proof state after:
no goals
Theorem: take_one_nil
Proof state before:
α : Type u_1
⊢ take 1 [] = []
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_length_cons_le_succ
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length (head :: tail) ≤ succ k → length tail ≤ k
Tactic:
rw [length]
Proof state after:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length tail + 1 ≤ succ k → length tail ≤ k
Theorem: list_length_cons_le_succ
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ length tail + 1 ≤ succ k → length tail ≤ k
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: list_take_all2
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length xs ≤ n → take n xs = xs
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → take n xs = xs
Theorem: list_take_all2
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → take n xs = xs
Tactic:
induction n with
| zero =>
  intro xs h
  rw [list_length_zero_or_smaller_is_empty xs h]
  rw [take]
| succ k ih =>
  intro xs
  cases xs with
  | nil =>
    intro _
    apply list_take_nil
  | cons head tail =>
    intro h
    rw [take]
    apply (congrArg (cons head))
    apply ih tail (list_length_cons_le_succ head tail k h)
Proof state after:
no goals
Theorem: list_take_all2
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), length xs ≤ zero → take zero xs = xs
Tactic:
intro xs h
Proof state after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero xs = xs
Theorem: list_take_all2
Proof state before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero xs = xs
Tactic:
rw [list_length_zero_or_smaller_is_empty xs h]
Proof state after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero [] = []
Theorem: list_take_all2
Proof state before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero [] = []
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_take_all2
Proof state before:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
⊢ ∀ (xs : List α), length xs ≤ succ k → take (succ k) xs = xs
Tactic:
intro xs
Proof state after:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
xs : List α
⊢ length xs ≤ succ k → take (succ k) xs = xs
Theorem: list_take_all2
Proof state before:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
xs : List α
⊢ length xs ≤ succ k → take (succ k) xs = xs
Tactic:
cases xs with
| nil =>
  intro _
  apply list_take_nil
| cons head tail =>
  intro h
  rw [take]
  apply (congrArg (cons head))
  apply ih tail (list_length_cons_le_succ head tail k h)
Proof state after:
no goals
Theorem: list_take_all2
Proof state before:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
⊢ length [] ≤ succ k → take (succ k) [] = []
Tactic:
intro _
Proof state after:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
a✝ : length [] ≤ succ k
⊢ take (succ k) [] = []
Theorem: list_take_all2
Proof state before:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
a✝ : length [] ≤ succ k
⊢ take (succ k) [] = []
Tactic:
apply list_take_nil
Proof state after:
no goals
Theorem: list_take_all2
Proof state before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
⊢ length (head :: tail) ≤ succ k → take (succ k) (head :: tail) = head :: tail
Tactic:
intro h
Proof state after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take (succ k) (head :: tail) = head :: tail
Theorem: list_take_all2
Proof state before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take (succ k) (head :: tail) = head :: tail
Tactic:
rw [take]
Proof state after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ head :: take k tail = head :: tail
Theorem: list_take_all2
Proof state before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ head :: take k tail = head :: tail
Tactic:
apply (congrArg (cons head))
Proof state after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take k tail = tail
Theorem: list_take_all2
Proof state before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take k tail = tail
Tactic:
apply ih tail (list_length_cons_le_succ head tail k h)
Proof state after:
no goals
Theorem: list_take_O
Proof state before:
α : Type u_1
xs : List α
⊢ take 0 xs = []
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_take_le_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) ≤ n
Tactic:
revert n
Proof state after:
α : Type u_1
xs : List α
⊢ ∀ (n : ℕ), length (take n xs) ≤ n
Theorem: list_take_le_length
Proof state before:
α : Type u_1
xs : List α
⊢ ∀ (n : ℕ), length (take n xs) ≤ n
Tactic:
induction xs with
| nil =>
  intro n
  rw [list_take_nil]
  simp
| cons head tail ih =>
  intro n
  cases n with
  | zero  =>
    rw [take]
    simp only [length_nil, zero_eq, le_refl]
  | succ k =>
    rw [take]
    rw [length]
    apply Nat.succ_le_succ
    apply (ih k)
Proof state after:
no goals
Theorem: list_take_le_length
Proof state before:
case nil
α : Type u_1
⊢ ∀ (n : ℕ), length (take n []) ≤ n
Tactic:
intro n
Proof state after:
case nil
α : Type u_1
n : ℕ
⊢ length (take n []) ≤ n
Theorem: list_take_le_length
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ length (take n []) ≤ n
Tactic:
rw [list_take_nil]
Proof state after:
case nil
α : Type u_1
n : ℕ
⊢ length [] ≤ n
Theorem: list_take_le_length
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ length [] ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: list_take_le_length
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ ∀ (n : ℕ), length (take n (head :: tail)) ≤ n
Tactic:
intro n
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
n : ℕ
⊢ length (take n (head :: tail)) ≤ n
Theorem: list_take_le_length
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
n : ℕ
⊢ length (take n (head :: tail)) ≤ n
Tactic:
cases n with
| zero  =>
  rw [take]
  simp only [length_nil, zero_eq, le_refl]
| succ k =>
  rw [take]
  rw [length]
  apply Nat.succ_le_succ
  apply (ih k)
Proof state after:
no goals
Theorem: list_take_le_length
Proof state before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length (take zero (head :: tail)) ≤ zero
Tactic:
rw [take]
Proof state after:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length [] ≤ zero
Theorem: list_take_le_length
Proof state before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
⊢ length [] ≤ zero
Tactic:
simp only [length_nil, zero_eq, le_refl]
Proof state after:
no goals
Theorem: list_take_le_length
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take (succ k) (head :: tail)) ≤ succ k
Tactic:
rw [take]
Proof state after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (head :: take k tail) ≤ succ k
Theorem: list_take_le_length
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (head :: take k tail) ≤ succ k
Tactic:
rw [length]
Proof state after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) + 1 ≤ succ k
Theorem: list_take_le_length
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) + 1 ≤ succ k
Tactic:
apply Nat.succ_le_succ
Proof state after:
case cons.succ.a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) ≤ k
Theorem: list_take_le_length
Proof state before:
case cons.succ.a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), length (take n tail) ≤ n
k : ℕ
⊢ length (take k tail) ≤ k
Tactic:
apply (ih k)
Proof state after:
no goals
Theorem: list_length_succ_le_cons
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ length tail → succ k ≤ length (head :: tail)
Tactic:
rw [length, <-nat_succ_eq_plus_one]
Proof state after:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ length tail → succ k ≤ succ (length tail)
Theorem: list_length_succ_le_cons
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ length tail → succ k ≤ succ (length tail)
Tactic:
apply Nat.succ_le_succ
Proof state after:
no goals
Theorem: list_length_pred_le_cons
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ length (head :: tail) → pred k ≤ length tail
Tactic:
rw [length, <-nat_succ_eq_plus_one]
Proof state after:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ succ (length tail) → pred k ≤ length tail
Theorem: list_length_pred_le_cons
Proof state before:
α : Type u_1
head : α
tail : List α
k : ℕ
⊢ k ≤ succ (length tail) → pred k ≤ length tail
Tactic:
apply nat_pred_le_succ
Proof state after:
no goals
Theorem: list_length_cons_succ
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
⊢ length (x :: xs) = succ (length xs)
Tactic:
simp
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ n ≤ length xs → length (take n xs) = n
Tactic:
revert n
Proof state after:
α : Type u_1
xs : List α
⊢ ∀ n ≤ length xs, length (take n xs) = n
Theorem: list_take_length_le
Proof state before:
α : Type u_1
xs : List α
⊢ ∀ n ≤ length xs, length (take n xs) = n
Tactic:
induction xs with
| nil =>
  intro n
  rw [list_take_nil]
  rw [length]
  cases n with
  | zero =>
    intro _
    rfl
  | succ n' =>
    intro h
    contradiction
| cons head tail ih =>
  intro n
  intro h
  have h' : _ := ih (pred n)
  have h₂ : _ := h' ((list_length_pred_le_cons head tail n) h)
  cases n with
  | zero => rw [list_take_zero, length]
  | succ n' =>
    simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
    rw [list_take_cons, list_length_cons_succ]
    simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
    exact h₂
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case nil
α : Type u_1
⊢ ∀ n ≤ length [], length (take n []) = n
Tactic:
intro n
Proof state after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length (take n []) = n
Theorem: list_take_length_le
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length (take n []) = n
Tactic:
rw [list_take_nil]
Proof state after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length [] = n
Theorem: list_take_length_le
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length [] = n
Tactic:
rw [length]
Proof state after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ 0 → 0 = n
Theorem: list_take_length_le
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ 0 → 0 = n
Tactic:
cases n with
| zero =>
  intro _
  rfl
| succ n' =>
  intro h
  contradiction
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case nil.zero
α : Type u_1
⊢ zero ≤ 0 → 0 = zero
Tactic:
intro _
Proof state after:
case nil.zero
α : Type u_1
a✝ : zero ≤ 0
⊢ 0 = zero
Theorem: list_take_length_le
Proof state before:
case nil.zero
α : Type u_1
a✝ : zero ≤ 0
⊢ 0 = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case nil.succ
α : Type u_1
n' : ℕ
⊢ succ n' ≤ 0 → 0 = succ n'
Tactic:
intro h
Proof state after:
case nil.succ
α : Type u_1
n' : ℕ
h : succ n' ≤ 0
⊢ 0 = succ n'
Theorem: list_take_length_le
Proof state before:
case nil.succ
α : Type u_1
n' : ℕ
h : succ n' ≤ 0
⊢ 0 = succ n'
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
⊢ ∀ n ≤ length (head :: tail), length (take n (head :: tail)) = n
Tactic:
intro n
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
⊢ n ≤ length (head :: tail) → length (take n (head :: tail)) = n
Theorem: list_take_length_le
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
⊢ n ≤ length (head :: tail) → length (take n (head :: tail)) = n
Tactic:
intro h
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
⊢ length (take n (head :: tail)) = n
Theorem: list_take_length_le
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
⊢ length (take n (head :: tail)) = n
Tactic:
have h' : _ := ih (pred n)
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Theorem: list_take_length_le
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Tactic:
have h₂ : _ := h' ((list_length_pred_le_cons head tail n) h)
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
h₂ : length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Theorem: list_take_length_le
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
h₂ : length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Tactic:
cases n with
| zero => rw [list_take_zero, length]
| succ n' =>
  simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
  rw [list_take_cons, list_length_cons_succ]
  simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
  exact h₂
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
h : zero ≤ length (head :: tail)
h' : pred zero ≤ length tail → length (take (pred zero) tail) = pred zero
h₂ : length (take (pred zero) tail) = pred zero
⊢ length (take zero (head :: tail)) = zero
Tactic:
rw [list_take_zero, length]
Proof state after:
no goals
Theorem: list_take_length_le
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : length (take (pred (succ n')) tail) = pred (succ n')
⊢ length (take (succ n') (head :: tail)) = succ n'
Tactic:
simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
Proof state after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ length (take (succ n') (head :: tail)) = succ n'
Theorem: list_take_length_le
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ length (take (succ n') (head :: tail)) = succ n'
Tactic:
rw [list_take_cons, list_length_cons_succ]
Proof state after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ succ (length (take n' tail)) = succ n'
Theorem: list_take_length_le
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ succ (length (take n' tail)) = succ n'
Tactic:
simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
Proof state after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ n' ≤ length tail
Theorem: list_take_length_le
Proof state before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ n' ≤ length tail
Tactic:
exact h₂
Proof state after:
no goals
Theorem: list_take_app
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
Tactic:
revert xs ys
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
Theorem: list_take_app
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
Tactic:
induction n with
| zero =>
  intro xs ys
  rw [Nat.zero_sub]
  repeat rw [take]
  simp only [append_nil]
| succ n ih =>
  intro xs ys
  cases xs with
  | nil =>
    repeat rw [take]
    simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
  | cons x xs =>
    rw [take]
    rw [length]
    rw [succ_sub_succ]
    rw [<- list_app_comm_cons]
    rw [take]
    apply (congrArg (cons x))
    apply ih
Proof state after:
no goals
Theorem: list_take_app
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs ys : List α), take zero (xs ++ ys) = take zero xs ++ take (zero - length xs) ys
Tactic:
intro xs ys
Proof state after:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take (zero - length xs) ys
Theorem: list_take_app
Proof state before:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take (zero - length xs) ys
Tactic:
rw [Nat.zero_sub]
Proof state after:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take 0 ys
Theorem: list_take_app
Proof state before:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take 0 ys
Tactic:
repeat rw [take]
Proof state after:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ []
Theorem: list_take_app
Proof state before:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ []
Tactic:
simp only [append_nil]
Proof state after:
no goals
Theorem: list_take_app
Proof state before:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ take 0 ys
Tactic:
rw [take]
Proof state after:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ []
Theorem: list_take_app
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
⊢ ∀ (xs ys : List α), take (succ n) (xs ++ ys) = take (succ n) xs ++ take (succ n - length xs) ys
Tactic:
intro xs ys
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
xs ys : List α
⊢ take (succ n) (xs ++ ys) = take (succ n) xs ++ take (succ n - length xs) ys
Theorem: list_take_app
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
xs ys : List α
⊢ take (succ n) (xs ++ ys) = take (succ n) xs ++ take (succ n - length xs) ys
Tactic:
cases xs with
| nil =>
  repeat rw [take]
  simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
| cons x xs =>
  rw [take]
  rw [length]
  rw [succ_sub_succ]
  rw [<- list_app_comm_cons]
  rw [take]
  apply (congrArg (cons x))
  apply ih
Proof state after:
no goals
Theorem: list_take_app
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = take (succ n) [] ++ take (succ n - length []) ys
Tactic:
repeat rw [take]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = [] ++ take (succ n - length []) ys
Theorem: list_take_app
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = [] ++ take (succ n - length []) ys
Tactic:
simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
Proof state after:
no goals
Theorem: list_take_app
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = take (succ n) [] ++ take (succ n - length []) ys
Tactic:
rw [take]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = [] ++ take (succ n - length []) ys
Theorem: list_take_app
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
x : α
xs : List α
⊢ take (succ n) (x :: xs ++ ys) = take (succ n) (x :: xs) ++ take (succ n - length (x :: xs)) ys
Tactic:
rw [take]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
x : α
xs : List α
⊢ take (succ n) (x :: xs ++ ys) = x :: take n xs ++ take (succ n - length (x :: xs)) ys
Theorem: list_take_app
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
x : α
xs : List α
⊢ take (succ n) (x :: xs ++ ys) = x :: take n xs ++ take (succ n - length (x :: xs)) ys
Tactic:
rw [length]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
x : α
xs : List α
⊢ take (succ n) (x :: xs ++ ys) = x :: take n xs ++ take (succ n - (length xs + 1)) ys