internlm/Lean-Github huggingface dataset:
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 n xs) = length (x :: xs) - succ n
Tactic:
rw [length]
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 xs + 1 - succ n
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 n xs) = length xs + 1 - succ n
Tactic:
rw [Nat.succ_sub_succ]
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 xs - n
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 n xs) = length xs - n
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_take_app_length
Proof state before:
α : Type u_1
xs ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
revert ys
Proof state after:
α : Type u_1
xs : List α
⊢ ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
Theorem: list_take_app_length
Proof state before:
α : Type u_1
xs : List α
⊢ ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
Tactic:
induction xs with
| nil =>
  simp only [take, forall_const]
| cons x xs ih =>
  intro ys
  rw [length]
  rw [<- list_app_comm_cons]
  rw [take]
  apply (congrArg (cons x))
  apply ih
Proof state after:
no goals
Theorem: list_take_app_length
Proof state before:
case nil
α : Type u_1
⊢ ∀ (ys : List α), take (length []) ([] ++ ys) = []
Tactic:
simp only [take, forall_const]
Proof state after:
no goals
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
⊢ ∀ (ys : List α), take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Tactic:
intro ys
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Tactic:
rw [length]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: xs ++ ys) = x :: xs
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: xs ++ ys) = x :: xs
Tactic:
rw [<- list_app_comm_cons]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: (xs ++ ys)) = x :: xs
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: (xs ++ ys)) = x :: xs
Tactic:
rw [take]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ x :: take (length xs) (xs ++ ys) = x :: xs
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ x :: take (length xs) (xs ++ ys) = x :: xs
Tactic:
apply (congrArg (cons x))
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Theorem: list_take_app_length
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
apply ih
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
α : Type u_1
xs : List α
n : ℕ
⊢ ∀ (ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
Tactic:
revert xs
Proof state after:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
Tactic:
induction n with
| zero =>
  intro xs ys zs hl ha
  have he := list_length_zero_is_empty _ hl
  rw [he]
  rw [he] at ha
  rw [take]
  rw [drop]
  rw [list_app_nil_l] at ha
  have ha' := Eq.symm ha
  constructor
  case left =>
    rfl
  case right =>
    exact ha'
| succ n ih =>
  intro xs ys zs hl ha
  cases xs with
  | nil =>
    rw [take]
    rw [drop]
    have ha' := Eq.symm ha
    rw [list_app_nil_nil] at ha'
    exact ha'
  | cons x xs =>
    rw [take, drop]
    cases ys with
    | nil =>
      rw [length] at hl
      contradiction
    | cons y ys =>
      simp only [length_cons, succ.injEq] at hl
      have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
        simp only [cons_append]
      rw [hzs] at ha
      rw [list_cons_eq] at ha
      cases ha with
      | intro hxy ha =>
        rw [hxy]
        have ih' := ih xs ys zs hl ha
        cases ih' with
        | intro hys hzs =>
          rw [<- hys]
          rw [<- hzs]
          simp only [and_self]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
⊢ ∀ (xs ys zs : List α), length ys = zero → xs = ys ++ zs → ys = take zero xs ∧ zs = drop zero xs
Tactic:
intro xs ys zs hl ha
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
⊢ ys = take zero xs ∧ zs = drop zero xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
⊢ ys = take zero xs ∧ zs = drop zero xs
Tactic:
have he := list_length_zero_is_empty _ hl
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ ys = take zero xs ∧ zs = drop zero xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ ys = take zero xs ∧ zs = drop zero xs
Tactic:
rw [he]
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Tactic:
rw [he] at ha
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Tactic:
rw [take]
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = drop zero xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = drop zero xs
Tactic:
rw [drop]
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Tactic:
rw [list_app_nil_l] at ha
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Tactic:
have ha' := Eq.symm ha
Proof state after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = [] ∧ zs = xs
Theorem: list_split_list
Proof state before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = [] ∧ zs = xs
Tactic:
constructor
Proof state after:
case zero.left
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []

case zero.right
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs
Theorem: list_split_list
Proof state before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []
Tactic:
case left =>
  rfl
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs
Tactic:
case right =>
  exact ha'
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs
Tactic:
exact ha'
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
⊢ ∀ (xs ys zs : List α), length ys = succ n → xs = ys ++ zs → ys = take (succ n) xs ∧ zs = drop (succ n) xs
Tactic:
intro xs ys zs hl ha
Proof state after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
xs ys zs : List α
hl : length ys = succ n
ha : xs = ys ++ zs
⊢ ys = take (succ n) xs ∧ zs = drop (succ n) xs
Theorem: list_split_list
Proof state before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
xs ys zs : List α
hl : length ys = succ n
ha : xs = ys ++ zs
⊢ ys = take (succ n) xs ∧ zs = drop (succ n) xs
Tactic:
cases xs with
| nil =>
  rw [take]
  rw [drop]
  have ha' := Eq.symm ha
  rw [list_app_nil_nil] at ha'
  exact ha'
| cons x xs =>
  rw [take, drop]
  cases ys with
  | nil =>
    rw [length] at hl
    contradiction
  | cons y ys =>
    simp only [length_cons, succ.injEq] at hl
    have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
      simp only [cons_append]
    rw [hzs] at ha
    rw [list_cons_eq] at ha
    cases ha with
    | intro hxy ha =>
      rw [hxy]
      have ih' := ih xs ys zs hl ha
      cases ih' with
      | intro hys hzs =>
        rw [<- hys]
        rw [<- hzs]
        simp only [and_self]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = take (succ n) [] ∧ zs = drop (succ n) []
Tactic:
rw [take]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = drop (succ n) []
Theorem: list_split_list
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = drop (succ n) []
Tactic:
rw [drop]
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = []
Theorem: list_split_list
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = []
Tactic:
have ha' := Eq.symm ha
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys ++ zs = []
⊢ ys = [] ∧ zs = []
Theorem: list_split_list
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys ++ zs = []
⊢ ys = [] ∧ zs = []
Tactic:
rw [list_app_nil_nil] at ha'
Proof state after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys = [] ∧ zs = []
⊢ ys = [] ∧ zs = []
Theorem: list_split_list
Proof state before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys = [] ∧ zs = []
⊢ ys = [] ∧ zs = []
Tactic:
exact ha'
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = take (succ n) (x :: xs) ∧ zs = drop (succ n) (x :: xs)
Tactic:
rw [take, drop]
Proof state after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = x :: take n xs ∧ zs = drop n xs
Tactic:
cases ys with
| nil =>
  rw [length] at hl
  contradiction
| cons y ys =>
  simp only [length_cons, succ.injEq] at hl
  have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
    simp only [cons_append]
  rw [hzs] at ha
  rw [list_cons_eq] at ha
  cases ha with
  | intro hxy ha =>
    rw [hxy]
    have ih' := ih xs ys zs hl ha
    cases ih' with
    | intro hys hzs =>
      rw [<- hys]
      rw [<- hzs]
      simp only [and_self]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : length [] = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [length] at hl
Proof state after:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : 0 = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : 0 = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length (y :: ys) = succ n
ha : x :: xs = y :: ys ++ zs
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
simp only [length_cons, succ.injEq] at hl
Proof state after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
  simp only [cons_append]
Proof state after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [hzs] at ha
Proof state after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: (ys ++ zs)
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: (ys ++ zs)
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [list_cons_eq] at ha
Proof state after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x = y ∧ xs = ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x = y ∧ xs = ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
cases ha with
| intro hxy ha =>
  rw [hxy]
  have ih' := ih xs ys zs hl ha
  cases ih' with
  | intro hys hzs =>
    rw [<- hys]
    rw [<- hzs]
    simp only [and_self]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys ++ zs = y :: (ys ++ zs)
Tactic:
simp only [cons_append]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [hxy]
Proof state after:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
have ih' := ih xs ys zs hl ha
Proof state after:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
ih' : ys = take n xs ∧ zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
ih' : ys = take n xs ∧ zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
cases ih' with
| intro hys hzs =>
  rw [<- hys]
  rw [<- hzs]
  simp only [and_self]
Proof state after:
no goals
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
rw [<- hys]
Proof state after:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = drop n xs
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = drop n xs
Tactic:
rw [<- hzs]
Proof state after:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = zs
Theorem: list_split_list
Proof state before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = zs
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: list_length_split
Proof state before:
α : Type u_1
xs ys : List α
⊢ length (xs ++ ys) = length xs + length ys
Tactic:
simp only [length_append]
Proof state after:
no goals
Theorem: list_prefix_leq_length
Proof state before:
α : Type u_1
xs ys zs : List α
⊢ xs = ys ++ zs → length ys ≤ length xs
Tactic:
intro xsyszs
Proof state after:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
⊢ length ys ≤ length xs
Theorem: list_prefix_leq_length
Proof state before:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
⊢ length ys ≤ length xs
Tactic:
have h := list_split_list xs (length ys) ys zs rfl xsyszs
Proof state after:
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
h : ys = take (length ys) xs ∧ zs = drop (length ys) xs
⊢ length ys ≤ length xs