internlm/Lean-Github huggingface dataset:
Theorem: list_prefix_leq_length
Proof state before:
α : 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
Tactic:
cases h with
| intro hys hzs =>
  rw [hzs] at xsyszs
  rw [xsyszs]
  rw [list_length_split]
  linarith
Proof state after:
no goals
Theorem: list_prefix_leq_length
Proof state before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ zs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs
Tactic:
rw [hzs] at xsyszs
Proof state after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs
Theorem: list_prefix_leq_length
Proof state before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length xs
Tactic:
rw [xsyszs]
Proof state after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length (ys ++ drop (length ys) xs)
Theorem: list_prefix_leq_length
Proof state before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length (ys ++ drop (length ys) xs)
Tactic:
rw [list_length_split]
Proof state after:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length ys + length (drop (length ys) xs)
Theorem: list_prefix_leq_length
Proof state before:
case intro
α : Type u_1
xs ys zs : List α
xsyszs : xs = ys ++ drop (length ys) xs
hys : ys = take (length ys) xs
hzs : zs = drop (length ys) xs
⊢ length ys ≤ length ys + length (drop (length ys) xs)
Tactic:
linarith
Proof state after:
no goals
Theorem: list_drop_length_prefix_is_suffix
Proof state before:
α : Type u_1
xs ys : List α
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
induction xs with
| nil =>
  simp only [drop, nil_append]
| cons x xs ih =>
  simp only [drop, add_eq, add_zero, append_eq]
  exact ih
Proof state after:
no goals
Theorem: list_drop_length_prefix_is_suffix
Proof state before:
case nil
α : Type u_1
ys : List α
⊢ drop (length []) ([] ++ ys) = ys
Tactic:
simp only [drop, nil_append]
Proof state after:
no goals
Theorem: list_drop_length_prefix_is_suffix
Proof state before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length (x :: xs)) (x :: xs ++ ys) = ys
Tactic:
simp only [drop, add_eq, add_zero, append_eq]
Proof state after:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length xs) (xs ++ ys) = ys
Theorem: list_drop_length_prefix_is_suffix
Proof state before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
exact ih
Proof state after:
no goals
Theorem: list_drop_app_length
Proof state before:
α : Type u_1
xs ys : List α
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
apply list_drop_length_prefix_is_suffix
Proof state after:
no goals
Theorem: list_drop_app
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ drop n (xs ++ ys) = drop n xs ++ drop (n - length xs) ys
Tactic:
sorry
Proof state after:
no goals
Theorem: list_take_length_prefix_is_prefix
Proof state before:
α : Type u_1
xs ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
induction xs with
| nil =>
  simp only [take]
| cons x xs ih =>
  simp only [take, add_eq, add_zero, append_eq, cons.injEq, true_and]
  exact ih
Proof state after:
no goals
Theorem: list_take_length_prefix_is_prefix
Proof state before:
case nil
α : Type u_1
ys : List α
⊢ take (length []) ([] ++ ys) = []
Tactic:
simp only [take]
Proof state after:
no goals
Theorem: list_take_length_prefix_is_prefix
Proof state before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : take (length xs) (xs ++ ys) = xs
⊢ take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Tactic:
simp only [take, add_eq, add_zero, append_eq, cons.injEq, true_and]
Proof state after:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : take (length xs) (xs ++ ys) = xs
⊢ take (length xs) (xs ++ ys) = xs
Theorem: list_take_length_prefix_is_prefix
Proof state before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : take (length xs) (xs ++ ys) = xs
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: list_prefix_length_leq
Proof state before:
α : Type u_1
⊢ ∀ (xs ys zs : List α), xs ++ ys = zs → length xs ≤ length zs
Tactic:
intro xs ys zs xsyszs
Proof state after:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ length xs ≤ length zs
Theorem: list_prefix_length_leq
Proof state before:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ length xs ≤ length zs
Tactic:
apply (list_prefix_leq_length zs xs ys)
Proof state after:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ zs = xs ++ ys
Theorem: list_prefix_length_leq
Proof state before:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ zs = xs ++ ys
Tactic:
apply Eq.symm
Proof state after:
case h
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ xs ++ ys = zs
Theorem: list_prefix_length_leq
Proof state before:
case h
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ xs ++ ys = zs
Tactic:
exact xsyszs
Proof state after:
no goals
Theorem: list_length_gt_zero
Proof state before:
α : Type u_1
⊢ ∀ (xs : List α), xs ≠ [] → 0 < length xs
Tactic:
intro xs
Proof state after:
α : Type u_1
xs : List α
⊢ xs ≠ [] → 0 < length xs
Theorem: list_length_gt_zero
Proof state before:
α : Type u_1
xs : List α
⊢ xs ≠ [] → 0 < length xs
Tactic:
cases xs with
| nil =>
  intro h
  contradiction
| cons x xs =>
  intro _
  rw [length]
  apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: list_length_gt_zero
Proof state before:
case nil
α : Type u_1
⊢ [] ≠ [] → 0 < length []
Tactic:
intro h
Proof state after:
case nil
α : Type u_1
h : [] ≠ []
⊢ 0 < length []
Theorem: list_length_gt_zero
Proof state before:
case nil
α : Type u_1
h : [] ≠ []
⊢ 0 < length []
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_length_gt_zero
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
⊢ x :: xs ≠ [] → 0 < length (x :: xs)
Tactic:
intro _
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length (x :: xs)
Theorem: list_length_gt_zero
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length (x :: xs)
Tactic:
rw [length]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length xs + 1
Theorem: list_length_gt_zero
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
a✝ : x :: xs ≠ []
⊢ 0 < length xs + 1
Tactic:
apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
⊢ ∀ (xs ys zs : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
intro xs ys zs
Proof state after:
α : Type u_1
xs ys zs : List α
⊢ xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
xs ys zs : List α
⊢ xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
revert xs ys
Proof state after:
α : Type u_1
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = zs → 0 < length xs ∧ length xs ≤ length zs
Tactic:
cases zs with
| nil =>
  intro xs ys hneq ha
  rw [list_app_nil_nil] at ha
  cases ha with
  | intro hxs hys =>
    contradiction
| cons z zs =>
  intro xs ys hneq ha
  have hl := list_length_gt_zero _ hneq
  rw [<- ha]
  apply And.intro
  case left =>
    exact hl
  case right =>
    rw [list_app_length]
    apply Nat.le_add_right
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case nil
α : Type u_1
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = [] → 0 < length xs ∧ length xs ≤ length []
Tactic:
intro xs ys hneq ha
Proof state after:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
rw [list_app_nil_nil] at ha
Proof state after:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs = [] ∧ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case nil
α : Type u_1
xs ys : List α
hneq : xs ≠ []
ha : xs = [] ∧ ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
cases ha with
| intro hxs hys =>
  contradiction
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case nil.intro
α : Type u_1
xs ys : List α
hneq : xs ≠ []
hxs : xs = []
hys : ys = []
⊢ 0 < length xs ∧ length xs ≤ length []
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case cons
α : Type u_1
z : α
zs : List α
⊢ ∀ (xs ys : List α), xs ≠ [] → xs ++ ys = z :: zs → 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
intro xs ys hneq ha
Proof state after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
have hl := list_length_gt_zero _ hneq
Proof state after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (z :: zs)
Tactic:
rw [<- ha]
Proof state after:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (xs ++ ys)
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
case cons
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs ∧ length xs ≤ length (xs ++ ys)
Tactic:
apply And.intro
Proof state after:
case cons.left
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs

case cons.right
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs
Tactic:
case left =>
  exact hl
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)
Tactic:
case right =>
  rw [list_app_length]
  apply Nat.le_add_right
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ 0 < length xs
Tactic:
exact hl
Proof state after:
no goals
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length (xs ++ ys)
Tactic:
rw [list_app_length]
Proof state after:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length xs + length ys
Theorem: list_prefix_is_gt_zero_and_leq
Proof state before:
α : Type u_1
z : α
zs xs ys : List α
hneq : xs ≠ []
ha : xs ++ ys = z :: zs
hl : 0 < length xs
⊢ length xs ≤ length xs + length ys
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
α : Type u_1
⊢ ∀ (xs : List α) (n : ℕ), 0 < n ∧ n ≤ length xs → take n xs ≠ []
Tactic:
intro xs n range h
Proof state after:
α : Type u_1
xs : List α
n : ℕ
range : 0 < n ∧ n ≤ length xs
h : take n xs = []
⊢ False
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
α : Type u_1
xs : List α
n : ℕ
range : 0 < n ∧ n ≤ length xs
h : take n xs = []
⊢ False
Tactic:
cases range with
| intro notzero max =>
  cases n with
  | zero =>
    contradiction
  | succ n =>
    cases xs with
    | nil =>
      contradiction
    | cons x xs =>
      simp only [succ_pos', take] at *
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
case intro
α : Type u_1
xs : List α
n : ℕ
h : take n xs = []
notzero : 0 < n
max : n ≤ length xs
⊢ False
Tactic:
cases n with
| zero =>
  contradiction
| succ n =>
  cases xs with
  | nil =>
    contradiction
  | cons x xs =>
    simp only [succ_pos', take] at *
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
case intro.zero
α : Type u_1
xs : List α
h : take zero xs = []
notzero : 0 < zero
max : zero ≤ length xs
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
case intro.succ
α : Type u_1
xs : List α
n : ℕ
h : take (succ n) xs = []
notzero : 0 < succ n
max : succ n ≤ length xs
⊢ False
Tactic:
cases xs with
| nil =>
  contradiction
| cons x xs =>
  simp only [succ_pos', take] at *
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
case intro.succ.nil
α : Type u_1
n : ℕ
notzero : 0 < succ n
h : take (succ n) [] = []
max : succ n ≤ length []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_prefix_is_not_empty_with_index_gt_zero
Proof state before:
case intro.succ.cons
α : Type u_1
n : ℕ
notzero : 0 < succ n
x : α
xs : List α
h : take (succ n) (x :: xs) = []
max : succ n ≤ length (x :: xs)
⊢ False
Tactic:
simp only [succ_pos', take] at *
Proof state after:
no goals
Theorem: list_app_uncons
Proof state before:
α : Type u_1
⊢ ∀ {x : α} {xs ys zs : List α},
    ys ++ zs = x :: xs → ys = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : ys = x :: ys'), ys' ++ zs = xs
Tactic:
intro x xs ys zs H
Proof state after:
α : Type u_1
x : α
xs ys zs : List α
H : ys ++ zs = x :: xs
⊢ ys = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : ys = x :: ys'), ys' ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case nil
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : [] = x :: ys'), ys' ++ zs = xs
Tactic:
apply Or.inl
Proof state after:
case nil.h
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs
Theorem: list_app_uncons
Proof state before:
case nil.h
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs
Tactic:
apply And.intro
Proof state after:
case nil.h.left
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = []

case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ zs = x :: xs
Theorem: list_app_uncons
Proof state before:
case nil.h.left
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_uncons
Proof state before:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ zs = x :: xs
Tactic:
simp only [nil_append] at H
Proof state after:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : zs = x :: xs
⊢ zs = x :: xs
Theorem: list_app_uncons
Proof state before:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : zs = x :: xs
⊢ zs = x :: xs
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_uncons
Proof state before:
case cons
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ y_ :: ys_ = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
apply Or.inr
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have H' := list_cons_eq.mp H
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have HR := H'.right
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have HL := H'.left
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
apply Exists.intro ys_
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : y_ :: ys_ = x :: ys_), ys_ ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : y_ :: ys_ = x :: ys_), ys_ ++ zs = xs
Tactic:
rw [HL]
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : x :: ys_ = x :: ys_), ys_ ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : x :: ys_ = x :: ys_), ys_ ++ zs = xs
Tactic:
apply Exists.intro rfl
Proof state after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ys_ ++ zs = xs
Theorem: list_app_uncons
Proof state before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ys_ ++ zs = xs
Tactic:
exact HR
Proof state after:
no goals
Theorem: list_app_inv_head
Proof state before:
α : Type u_1
⊢ ∀ {xs ys zs : List α}, xs ++ ys = xs ++ zs → ys = zs
Tactic:
intro xs ys zs H
Proof state after:
α : Type u_1
xs ys zs : List α
H : xs ++ ys = xs ++ zs
⊢ ys = zs
Theorem: list_app_inv_head
Proof state before:
α : Type u_1
xs ys zs : List α
H : xs ++ ys = xs ++ zs
⊢ ys = zs
Tactic:
simp only [append_cancel_left_eq] at H
Proof state after:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ ys = zs
Theorem: list_app_inv_head
Proof state before:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ ys = zs
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_inv_head_reverse
Proof state before:
α : Type u_1
⊢ ∀ {xs ys zs : List α}, ys = zs → xs ++ ys = xs ++ zs
Tactic:
intro xs ys zs H
Proof state after:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ xs ++ ys = xs ++ zs
Theorem: list_app_inv_head_reverse
Proof state before:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ xs ++ ys = xs ++ zs
Tactic:
simp only [append_cancel_left_eq]
Proof state after:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ ys = zs
Theorem: list_app_inv_head_reverse
Proof state before:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ ys = zs
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_inv_tail
Proof state before:
α : Type u_1
⊢ ∀ {xs ys zs : List α}, xs ++ zs = ys ++ zs → xs = ys
Tactic:
intro xs ys zs H
Proof state after:
α : Type u_1
xs ys zs : List α
H : xs ++ zs = ys ++ zs
⊢ xs = ys
Theorem: list_app_inv_tail
Proof state before:
α : Type u_1
xs ys zs : List α
H : xs ++ zs = ys ++ zs
⊢ xs = ys
Tactic:
simp only [append_cancel_right_eq] at H
Proof state after:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys
Theorem: list_app_inv_tail
Proof state before:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_inv_tail_reverse
Proof state before:
α : Type u_1
⊢ ∀ {xs ys zs : List α}, xs = ys → xs ++ zs = ys ++ zs
Tactic:
intro xs ys zs H
Proof state after:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs ++ zs = ys ++ zs
Theorem: list_app_inv_tail_reverse
Proof state before:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs ++ zs = ys ++ zs
Tactic:
simp only [append_cancel_right_eq]
Proof state after:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys
Theorem: list_app_inv_tail_reverse
Proof state before:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys
Tactic:
assumption
Proof state after:
no goals
Theorem: nat_min_zero
Proof state before:
n : Nat
⊢ min 0 n = 0
Tactic:
unfold min
Proof state after:
n : Nat
⊢ instMinNat.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : Nat
⊢ instMinNat.1 0 n = 0
Tactic:
unfold instMinNat
Proof state after:
n : Nat
⊢ minOfLe.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : Nat
⊢ minOfLe.1 0 n = 0
Tactic:
unfold minOfLe
Proof state after:
n : Nat
⊢ { min := fun x y => if x ≤ y then x else y }.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : Nat
⊢ { min := fun x y => if x ≤ y then x else y }.1 0 n = 0
Tactic:
simp
Proof state after:
no goals
Theorem: nat_min_zero'
Proof state before:
n : Nat
⊢ min 0 n = 0
Tactic:
simp
Proof state after:
no goals
Theorem: nullable_emptySet
Proof state before:
⊢ (α : Type) → ν' ∅ ≡ PEmpty.{1}
Tactic:
intro α
Proof state after:
α : Type
⊢ ν' ∅ ≡ PEmpty.{1}
Theorem: nullable_emptySet
Proof state before:
α : Type
⊢ ν' ∅ ≡ PEmpty.{1}
Tactic:
constructor
Proof state after:
case a
α : Type
⊢ ν' ∅ = PEmpty.{1}
Theorem: nullable_emptySet
Proof state before:
case a
α : Type
⊢ ν' ∅ = PEmpty.{1}
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_universal
Proof state before:
⊢ (α : Type) → ν' 𝒰 ≡ PUnit.{1}
Tactic:
intro α
Proof state after:
α : Type
⊢ ν' 𝒰 ≡ PUnit.{1}
Theorem: nullable_universal
Proof state before:
α : Type
⊢ ν' 𝒰 ≡ PUnit.{1}
Tactic:
constructor
Proof state after:
case a
α : Type
⊢ ν' 𝒰 = PUnit.{1}
Theorem: nullable_universal
Proof state before:
case a
α : Type
⊢ ν' 𝒰 = PUnit.{1}
Tactic:
rfl
Proof state after:
no goals
Theorem: nullable_emptyStr
Proof state before:
⊢ (α : Type) → ν' ε ≃ PUnit.{u_1}
Tactic:
intro α
Proof state after:
α : Type
⊢ ν' ε ≃ PUnit.{u_1}
Theorem: nullable_emptyStr
Proof state before:
α : Type
⊢ ν' ε ≃ PUnit.{u_1}
Tactic:
refine Equiv.mk ?a ?b ?c ?d
Proof state after:
case a
α : Type
⊢ ν' ε → PUnit.{u_1}

case b
α : Type
⊢ PUnit.{u_1} → ν' ε

case c
α : Type
⊢ Function.LeftInverse ?b ?a

case d
α : Type
⊢ Function.RightInverse ?b ?a