internlm/Lean-Github huggingface dataset:
Theorem: list_drop_all2
Proof state before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero xs = []
Tactic:
rw [empty_list]
Proof state after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero [] = []
Theorem: list_drop_all2
Proof state before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
empty_list : xs = []
⊢ drop zero [] = []
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_all2
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ ∀ (xs : List α), length xs ≤ succ n → drop (succ n) xs = []
Tactic:
intro xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
xs : List α
⊢ length xs ≤ succ n → drop (succ n) xs = []
Theorem: list_drop_all2
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
xs : List α
⊢ length xs ≤ succ n → drop (succ n) xs = []
Tactic:
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 succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ length [] ≤ succ n → drop (succ n) [] = []
Tactic:
rw [length]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ 0 ≤ succ n → drop (succ n) [] = []
Theorem: list_drop_all2
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
⊢ 0 ≤ succ n → drop (succ n) [] = []
Tactic:
intro _
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
a✝ : 0 ≤ succ n
⊢ drop (succ n) [] = []
Theorem: list_drop_all2
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
a✝ : 0 ≤ succ n
⊢ drop (succ n) [] = []
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: list_drop_all2
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length (x :: xs) ≤ succ n → drop (succ n) (x :: xs) = []
Tactic:
rw [length]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length xs + 1 ≤ succ n → drop (succ n) (x :: xs) = []
Theorem: list_drop_all2
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
⊢ length xs + 1 ≤ succ n → drop (succ n) (x :: xs) = []
Tactic:
intro h
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop (succ n) (x :: xs) = []
Theorem: list_drop_all2
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop (succ n) (x :: xs) = []
Tactic:
rw [drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop n xs = []
Theorem: list_drop_all2
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs + 1 ≤ succ n
⊢ drop n xs = []
Tactic:
rw [nat_succ_le_succ_iff] at h
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs ≤ n
⊢ drop n xs = []
Theorem: list_drop_all2
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length xs ≤ n → drop n xs = []
x : α
xs : List α
h : length xs ≤ n
⊢ drop n xs = []
Tactic:
exact ih xs h
Proof state after:
no goals
Theorem: list_take_drop
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ take n xs ++ drop n xs = xs
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), take n xs ++ drop n xs = xs
Theorem: list_take_drop
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), take n xs ++ drop n xs = xs
Tactic:
induction n with
| zero =>
  intro xs
  rw [take]
  rw [drop]
  rw [list_app_nil_l]
| succ n ih =>
  intro xs
  cases xs with
  | nil =>
    rw [take, drop]
    simp only [append_nil]
  | cons x xs =>
    rw [take, drop]
    apply (congrArg (cons x))
    apply ih
Proof state after:
no goals
Theorem: list_take_drop
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), take zero xs ++ drop zero xs = xs
Tactic:
intro xs
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ take zero xs ++ drop zero xs = xs
Theorem: list_take_drop
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ take zero xs ++ drop zero xs = xs
Tactic:
rw [take]
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ [] ++ drop zero xs = xs
Theorem: list_take_drop
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ [] ++ drop zero xs = xs
Tactic:
rw [drop]
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ [] ++ xs = xs
Theorem: list_take_drop
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ [] ++ xs = xs
Tactic:
rw [list_app_nil_l]
Proof state after:
no goals
Theorem: list_take_drop
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ ∀ (xs : List α), take (succ n) xs ++ drop (succ n) xs = xs
Tactic:
intro xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
xs : List α
⊢ take (succ n) xs ++ drop (succ n) xs = xs
Theorem: list_take_drop
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
xs : List α
⊢ take (succ n) xs ++ drop (succ n) xs = xs
Tactic:
cases xs with
| nil =>
  rw [take, drop]
  simp only [append_nil]
| cons x xs =>
  rw [take, drop]
  apply (congrArg (cons x))
  apply ih
Proof state after:
no goals
Theorem: list_take_drop
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ take (succ n) [] ++ drop (succ n) [] = []
Tactic:
rw [take, drop]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ [] ++ [] = []
Theorem: list_take_drop
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ [] ++ [] = []
Tactic:
simp only [append_nil]
Proof state after:
no goals
Theorem: list_take_drop
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ take (succ n) (x :: xs) ++ drop (succ n) (x :: xs) = x :: xs
Tactic:
rw [take, drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ x :: take n xs ++ drop n xs = x :: xs
Theorem: list_take_drop
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ x :: take n xs ++ drop n xs = x :: xs
Tactic:
apply (congrArg (cons x))
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ List.append (take n xs) (drop n xs) = xs
Theorem: list_take_drop
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ List.append (take n xs) (drop n xs) = xs
Tactic:
apply ih
Proof state after:
no goals
Theorem: nat_succ_gt_succ
Proof state before:
n m : ℕ
⊢ succ n > succ m → n > m
Tactic:
intro h
Proof state after:
n m : ℕ
h : succ n > succ m
⊢ n > m
Theorem: nat_succ_gt_succ
Proof state before:
n m : ℕ
h : succ n > succ m
⊢ n > m
Tactic:
cases h with
| refl =>
  constructor
| step s =>
  apply Nat.le_of_succ_le_succ
  exact (Nat.le_succ_of_le s)
Proof state after:
no goals
Theorem: nat_succ_gt_succ
Proof state before:
case refl
m : ℕ
⊢ succ m > m
Tactic:
constructor
Proof state after:
no goals
Theorem: nat_succ_gt_succ
Proof state before:
case step
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ n > m
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
case step.a
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ succ (succ m) ≤ succ n
Theorem: nat_succ_gt_succ
Proof state before:
case step.a
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ succ (succ m) ≤ succ n
Tactic:
exact (Nat.le_succ_of_le s)
Proof state after:
no goals
Theorem: nat_succ_gt_succ'
Proof state before:
n m : ℕ
⊢ succ n > succ m → n > m
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ n > length xs → length (take n xs) = length xs
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
Theorem: list_take_large_length
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
Tactic:
induction n with
| zero =>
  intro xs
  intro h
  contradiction
| succ n ih =>
  intro xs
  intro h
  cases xs with
  | nil =>
    rw [take]
  | cons x xs =>
    rw [take]
    repeat rw [length]
    apply congrArg succ
    rw [length] at h
    have h' := nat_succ_gt_succ h
    exact ih h'
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
case zero
α : Type u_1
⊢ ∀ {xs : List α}, zero > length xs → length (take zero xs) = length xs
Tactic:
intro xs
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ zero > length xs → length (take zero xs) = length xs
Theorem: list_take_large_length
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ zero > length xs → length (take zero xs) = length xs
Tactic:
intro h
Proof state after:
case zero
α : Type u_1
xs : List α
h : zero > length xs
⊢ length (take zero xs) = length xs
Theorem: list_take_large_length
Proof state before:
case zero
α : Type u_1
xs : List α
h : zero > length xs
⊢ length (take zero xs) = length xs
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
⊢ ∀ {xs : List α}, succ n > length xs → length (take (succ n) xs) = length xs
Tactic:
intro xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
⊢ succ n > length xs → length (take (succ n) xs) = length xs
Theorem: list_take_large_length
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
⊢ succ n > length xs → length (take (succ n) xs) = length xs
Tactic:
intro h
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
h : succ n > length xs
⊢ length (take (succ n) xs) = length xs
Theorem: list_take_large_length
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
h : succ n > length xs
⊢ length (take (succ n) xs) = length xs
Tactic:
cases xs with
| nil =>
  rw [take]
| cons x xs =>
  rw [take]
  repeat rw [length]
  apply congrArg succ
  rw [length] at h
  have h' := nat_succ_gt_succ h
  exact ih h'
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
h : succ n > length []
⊢ length (take (succ n) []) = length []
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take (succ n) (x :: xs)) = length (x :: xs)
Tactic:
rw [take]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (x :: take n xs) = length (x :: xs)
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (x :: take n xs) = length (x :: xs)
Tactic:
repeat rw [length]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1
Tactic:
apply congrArg succ
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) = length xs
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) = length xs
Tactic:
rw [length] at h
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
⊢ length (take n xs) = length xs
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
⊢ length (take n xs) = length xs
Tactic:
have h' := nat_succ_gt_succ h
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
h' : n > length xs
⊢ length (take n xs) = length xs
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
h' : n > length xs
⊢ length (take n xs) = length xs
Tactic:
exact ih h'
Proof state after:
no goals
Theorem: list_take_large_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length (x :: xs)
Tactic:
rw [length]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = min n (length xs)
Tactic:
unfold min
Proof state after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = instMinNat.1 n (length xs)
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = instMinNat.1 n (length xs)
Tactic:
unfold instMinNat
Proof state after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = minOfLe.1 n (length xs)
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = minOfLe.1 n (length xs)
Tactic:
unfold minOfLe
Proof state after:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = { min := fun x y => if x ≤ y then x else y }.1 n (length xs)
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (take n xs) = { min := fun x y => if x ≤ y then x else y }.1 n (length xs)
Tactic:
simp only [length_take, ge_iff_le]
Proof state after:
α : Type u_1
n : ℕ
xs : List α
⊢ min n (length xs) = if n ≤ length xs then n else length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ min n (length xs) = if n ≤ length xs then n else length xs
Tactic:
split
Proof state after:
case inl
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n

case inr
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
case inl =>
  rename_i c
  unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_left_iff, not_le]
  intro c'
  linarith
Proof state after:
no goals
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
case inr =>
  rename_i c
  have c' := gt_of_not_le c
  unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_right_iff]
  intro c''
  linarith
Proof state after:
no goals
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
h✝ : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
rename_i c
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ min n (length xs) = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ min n (length xs) = n
Tactic:
unfold min
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ instMinNat.1 n (length xs) = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ instMinNat.1 n (length xs) = n
Tactic:
unfold instMinNat
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ minOfLe.1 n (length xs) = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ minOfLe.1 n (length xs) = n
Tactic:
unfold minOfLe
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = n
Tactic:
simp only [ite_eq_left_iff, not_le]
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ length xs < n → length xs = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
⊢ length xs < n → length xs = n
Tactic:
intro c'
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
c' : length xs < n
⊢ length xs = n
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : n ≤ length xs
c' : length xs < n
⊢ length xs = n
Tactic:
linarith
Proof state after:
no goals
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
h✝ : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
rename_i c
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
⊢ min n (length xs) = length xs
Tactic:
have c' := gt_of_not_le c
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ min n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ min n (length xs) = length xs
Tactic:
unfold min
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ instMinNat.1 n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ instMinNat.1 n (length xs) = length xs
Tactic:
unfold instMinNat
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ minOfLe.1 n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ minOfLe.1 n (length xs) = length xs
Tactic:
unfold minOfLe
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ { min := fun x y => if x ≤ y then x else y }.1 n (length xs) = length xs
Tactic:
simp only [ite_eq_right_iff]
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ n ≤ length xs → n = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
⊢ n ≤ length xs → n = length xs
Tactic:
intro c''
Proof state after:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
c'' : n ≤ length xs
⊢ n = length xs
Theorem: list_take_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
c : ¬n ≤ length xs
c' : n > length xs
c'' : n ≤ length xs
⊢ n = length xs
Tactic:
linarith
Proof state after:
no goals
Theorem: list_drop_length
Proof state before:
α : Type u_1
n : ℕ
xs : List α
⊢ length (drop n xs) = length xs - n
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length (drop n xs) = length xs - n
Theorem: list_drop_length
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length (drop n xs) = length xs - n
Tactic:
induction n with
| zero =>
  intro xs
  rw [drop]
  rw [Nat.sub_zero]
| succ n ih =>
  intro xs
  cases xs with
  | nil =>
    rw [drop]
    rw [length]
    rw [Nat.zero_sub]
  | cons x xs =>
    rw [drop]
    rw [length]
    rw [Nat.succ_sub_succ]
    apply ih
Proof state after:
no goals
Theorem: list_drop_length
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), length (drop zero xs) = length xs - zero
Tactic:
intro xs
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ length (drop zero xs) = length xs - zero
Theorem: list_drop_length
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ length (drop zero xs) = length xs - zero
Tactic:
rw [drop]
Proof state after:
case zero
α : Type u_1
xs : List α
⊢ length xs = length xs - zero
Theorem: list_drop_length
Proof state before:
case zero
α : Type u_1
xs : List α
⊢ length xs = length xs - zero
Tactic:
rw [Nat.sub_zero]
Proof state after:
no goals
Theorem: list_drop_length
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ ∀ (xs : List α), length (drop (succ n) xs) = length xs - succ n
Tactic:
intro xs
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
xs : List α
⊢ length (drop (succ n) xs) = length xs - succ n
Theorem: list_drop_length
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
xs : List α
⊢ length (drop (succ n) xs) = length xs - succ n
Tactic:
cases xs with
| nil =>
  rw [drop]
  rw [length]
  rw [Nat.zero_sub]
| cons x xs =>
  rw [drop]
  rw [length]
  rw [Nat.succ_sub_succ]
  apply ih
Proof state after:
no goals
Theorem: list_drop_length
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ length (drop (succ n) []) = length [] - succ n
Tactic:
rw [drop]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ length [] = length [] - succ n
Theorem: list_drop_length
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ length [] = length [] - succ n
Tactic:
rw [length]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ 0 = 0 - succ n
Theorem: list_drop_length
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ 0 = 0 - succ n
Tactic:
rw [Nat.zero_sub]
Proof state after:
no goals
Theorem: list_drop_length
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
x : α
xs : List α
⊢ length (drop (succ n) (x :: xs)) = length (x :: xs) - succ n
Tactic:
rw [drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
x : α
xs : List α
⊢ length (drop n xs) = length (x :: xs) - succ n