internlm/Lean-Github huggingface dataset:
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 xs + 1)) ys
Tactic:
rw [succ_sub_succ]
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 (n - length 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 (n - length xs) ys
Tactic:
rw [<- list_app_comm_cons]
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 (n - length 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 (n - length 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 α
⊢ x :: take n (xs ++ ys) = x :: take n xs ++ take (n - length 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 α
⊢ x :: take n (xs ++ ys) = x :: take n xs ++ take (n - length xs) ys
Tactic:
apply (congrArg (cons x))
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 n (xs ++ ys) = List.append (take n xs) (take (n - length 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 n (xs ++ ys) = List.append (take n xs) (take (n - length xs) ys)
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_take_app_2
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ take (length xs + n) (xs ++ ys) = xs ++ take n ys
Tactic:
induction xs with
| nil =>
  simp only [length_nil, zero_add, nil_append]
| cons x xs ih =>
  rw [<- list_app_comm_cons]
  rw [length]
  have hcomm: length xs + 1 + n = succ (length xs + n) := by
    rw [Nat.add_comm (length xs) 1]
    rw [Nat.add_assoc]
    rw [Nat.add_comm]
  rw [hcomm]
  rw [take]
  apply (congrArg (cons x))
  apply ih
Proof state after:
no goals
Theorem: list_take_app_2
Proof state before:
case nil
α : Type u_1
n : ℕ
ys : List α
⊢ take (length [] + n) ([] ++ ys) = [] ++ take n ys
Tactic:
simp only [length_nil, zero_add, nil_append]
Proof state after:
no goals
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length (x :: xs) + n) (x :: xs ++ ys) = x :: xs ++ take n ys
Tactic:
rw [<- list_app_comm_cons]
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length (x :: xs) + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length (x :: xs) + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Tactic:
rw [length]
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Tactic:
have hcomm: length xs + 1 + n = succ (length xs + n) := by
  rw [Nat.add_comm (length xs) 1]
  rw [Nat.add_assoc]
  rw [Nat.add_comm]
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Tactic:
rw [hcomm]
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (succ (length xs + n)) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (succ (length xs + n)) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Tactic:
rw [take]
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ x :: take (length xs + n) (xs ++ ys) = x :: xs ++ take n ys
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ x :: take (length xs + n) (xs ++ ys) = x :: xs ++ take n ys
Tactic:
apply (congrArg (cons x))
Proof state after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + n) (xs ++ ys) = List.append xs (take n ys)
Theorem: list_take_app_2
Proof state before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + n) (xs ++ ys) = List.append xs (take n ys)
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_take_app_2
Proof state before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ length xs + 1 + n = succ (length xs + n)
Tactic:
rw [Nat.add_comm (length xs) 1]
Proof state after:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + length xs + n = succ (length xs + n)
Theorem: list_take_app_2
Proof state before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + length xs + n = succ (length xs + n)
Tactic:
rw [Nat.add_assoc]
Proof state after:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + (length xs + n) = succ (length xs + n)
Theorem: list_take_app_2
Proof state before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + (length xs + n) = succ (length xs + n)
Tactic:
rw [Nat.add_comm]
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
α : Type u_1
m n✝ n : ℕ
xs : List α
⊢ take n (take m xs) = take (min n m) xs
Tactic:
revert m xs
Proof state after:
α : Type u_1
n✝ n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
Theorem: list_take_take
Proof state before:
α : Type u_1
n✝ n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
Tactic:
induction n with
| zero =>
  intro m xs
  rw [nat_min_zero]
  repeat rw [take]
| succ n ihn =>
  intro m xs
  cases m with
  | zero =>
    unfold min
    unfold instMinNat
    unfold minOfLe
    rw [take]
    simp only [take]
  | succ m =>
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only
    split
    case succ.succ.inl h =>
      rw [nat_succ_le_succ_iff] at h
      cases xs with
      | nil =>
        rw [take]
      | cons x xs =>
        repeat rw [take]
        apply (congrArg (cons x))
        have hmin : min n m = n := by
          unfold min
          unfold instMinNat
          unfold minOfLe
          simp only [ite_eq_left_iff, not_le]
          intro hless
          linarith
        have ihn' : _ := @ihn m xs
        rw [hmin] at ihn'
        exact ihn'
    case succ.succ.inr h =>
      rw [nat_succ_le_succ_iff] at h
      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 zero
α : Type u_1
n : ℕ
⊢ ∀ {m : ℕ} (xs : List α), take zero (take m xs) = take (min zero m) xs
Tactic:
intro m xs
Proof state after:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take (min zero m) xs
Theorem: list_take_take
Proof state before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take (min zero m) xs
Tactic:
rw [nat_min_zero]
Proof state after:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take 0 xs
Theorem: list_take_take
Proof state before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ take zero (take m xs) = take 0 xs
Tactic:
repeat rw [take]
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case zero
α : Type u_1
n m : ℕ
xs : List α
⊢ [] = take 0 xs
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
⊢ ∀ {m : ℕ} (xs : List α), take (succ n) (take m xs) = take (min (succ n) m) xs
Tactic:
intro m xs
Proof state after:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
xs : List α
⊢ take (succ n) (take m xs) = take (min (succ n) m) xs
Theorem: list_take_take
Proof state before:
case succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
m : ℕ
xs : List α
⊢ take (succ n) (take m xs) = take (min (succ n) m) xs
Tactic:
cases m with
| zero =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  rw [take]
  simp only [take]
| succ m =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only
  split
  case succ.succ.inl h =>
    rw [nat_succ_le_succ_iff] at h
    cases xs with
    | nil =>
      rw [take]
    | cons x xs =>
      repeat rw [take]
      apply (congrArg (cons x))
      have hmin : min n m = n := by
        unfold min
        unfold instMinNat
        unfold minOfLe
        simp only [ite_eq_left_iff, not_le]
        intro hless
        linarith
      have ihn' : _ := @ihn m xs
      rw [hmin] at ihn'
      exact ihn'
  case succ.succ.inr h =>
    rw [nat_succ_le_succ_iff] at h
    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 succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (min (succ n) zero) xs
Tactic:
unfold min
Proof state after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (instMinNat.1 (succ n) zero) xs
Theorem: list_take_take
Proof state before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (instMinNat.1 (succ n) zero) xs
Tactic:
unfold instMinNat
Proof state after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (minOfLe.1 (succ n) zero) xs
Theorem: list_take_take
Proof state before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take (minOfLe.1 (succ n) zero) xs
Tactic:
unfold minOfLe
Proof state after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Theorem: list_take_take
Proof state before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) (take zero xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Tactic:
rw [take]
Proof state after:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) [] = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Theorem: list_take_take
Proof state before:
case succ.zero
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
⊢ take (succ n) [] = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) zero) xs
Tactic:
simp only [take]
Proof state after:
no goals
Theorem: list_take_take
Proof state before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (min (succ n) (succ m)) xs
Tactic:
unfold min
Proof state after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (instMinNat.1 (succ n) (succ m)) xs
Theorem: list_take_take
Proof state before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (instMinNat.1 (succ n) (succ m)) xs
Tactic:
unfold instMinNat
Proof state after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (minOfLe.1 (succ n) (succ m)) xs
Theorem: list_take_take
Proof state before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (minOfLe.1 (succ n) (succ m)) xs
Tactic:
unfold minOfLe
Proof state after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) (succ m)) xs
Theorem: list_take_take
Proof state before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take ({ min := fun x y => if x ≤ y then x else y }.1 (succ n) (succ m)) xs
Tactic:
simp only
Proof state after:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (if succ n ≤ succ m then succ n else succ m) xs
Theorem: list_take_take
Proof state before:
case succ.succ
α : Type u_1
n✝ n : ℕ
ihn : ∀ {m : ℕ} (xs : List α), take n (take m xs) = take (min n m) xs
xs : List α
m : ℕ
⊢ take (succ n) (take (succ m) xs) = take (if succ n ≤ succ m then succ n else succ m) xs
Tactic:
split
Proof state after:
case succ.succ.inl
α : 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 n) xs

case succ.succ.inr
α : 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
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 n) xs
Tactic:
case succ.succ.inl h =>
  rw [nat_succ_le_succ_iff] at h
  cases xs with
  | nil =>
    rw [take]
  | cons x xs =>
    repeat rw [take]
    apply (congrArg (cons x))
    have hmin : min n m = n := by
      unfold min
      unfold instMinNat
      unfold minOfLe
      simp only [ite_eq_left_iff, not_le]
      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:
α : 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:
case succ.succ.inr h =>
  rw [nat_succ_le_succ_iff] at h
  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:
α : 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 n) 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 n) 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 n) xs
Tactic:
cases xs with
| nil =>
  rw [take]
| cons x xs =>
  repeat rw [take]
  apply (congrArg (cons x))
  have hmin : min n m = n := by
    unfold min
    unfold instMinNat
    unfold minOfLe
    simp only [ite_eq_left_iff, not_le]
    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 n) []
Tactic:
rw [take]
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 n) (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 n 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 n 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 n 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 n xs
Tactic:
have hmin : min n m = n := by
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [ite_eq_left_iff, not_le]
  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 = n
⊢ take n (take m xs) = take n 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 = n
⊢ take n (take m xs) = take n 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 = n
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take n 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 = n
ihn' : take n (take m xs) = take (min n m) xs
⊢ take n (take m xs) = take n 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 = n
ihn' : take n (take m xs) = take n xs
⊢ take n (take m xs) = take n 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 = n
ihn' : take n (take m xs) = take n xs
⊢ take n (take m xs) = take n 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 α
⊢ x :: take n (take m xs) = take (succ n) (x :: 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 n 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 = n
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 = 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 α
⊢ instMinNat.1 n m = n
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 = 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 α
⊢ minOfLe.1 n m = n
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 = n