internlm/Lean-Github huggingface dataset:
Theorem: list_app_eq_unit
Proof state before:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []
Tactic:
rw [h1]
Proof state after:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ a :: tail = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ a :: tail = [a] ∧ ys = []
Tactic:
cases h2 with
| intro h4 h5 =>
  rw [h4, h5]
  apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ a :: tail = [a] ∧ ys = []
Tactic:
rw [h4, h5]
Proof state after:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ [a] = [a] ∧ [] = []
Theorem: list_app_eq_unit
Proof state before:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ [a] = [a] ∧ [] = []
Tactic:
apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_eq_unit_app
Proof state before:
α : Type u_1
a : α
xs ys : List α
⊢ [a] = xs ++ ys → xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
intro H
Proof state after:
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Theorem: list_eq_unit_app
Proof state before:
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
apply list_app_eq_unit
Proof state after:
case a
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs ++ ys = [a]
Theorem: list_eq_unit_app
Proof state before:
case a
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs ++ ys = [a]
Tactic:
apply Eq.symm
Proof state after:
case a.h
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ [a] = xs ++ ys
Theorem: list_eq_unit_app
Proof state before:
case a.h
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ [a] = xs ++ ys
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
α : Type u_1
xs ys : List α
x y : α
⊢ xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y
Tactic:
revert ys
Proof state after:
α : Type u_1
xs : List α
x y : α
⊢ ∀ {ys : List α}, xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
α : Type u_1
xs : List α
x y : α
⊢ ∀ {ys : List α}, xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y
Tactic:
induction xs with
| nil =>
  intro ys h'
  simp only [nil_append] at h'
  have h3: (ys = [] /\ [y] = [x]) \/ (ys = [x] /\ [y] = []) := list_app_eq_unit (Eq.symm h')
  cases h3 with | inl left =>
    cases left with
    | intro empty xy =>
      simp only [cons.injEq, and_true] at xy
      rw [empty, xy]
      apply And.intro <;> rfl
  | inr right =>
    cases right with
    | intro empty ysx =>
      contradiction
| cons headx tailx ihx =>
  intro ys
  cases ys with
  | nil =>
    intro h'
    simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
  | cons heady taily =>
    intro h'
    simp only [cons_append, cons.injEq] at h'
    cases h' with
    | intro heads tails =>
      rw [heads]
      have h: tailx = taily ∧ x = y := (ihx tails)
      cases h with
      | intro tailxy xy =>
        rw [tailxy]
        rw [xy]
        apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case nil
α : Type u_1
x y : α
⊢ ∀ {ys : List α}, [] ++ [x] = ys ++ [y] → [] = ys ∧ x = y
Tactic:
intro ys h'
Proof state after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [] ++ [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [] ++ [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Tactic:
simp only [nil_append] at h'
Proof state after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Tactic:
have h3: (ys = [] /\ [y] = [x]) \/ (ys = [x] /\ [y] = []) := list_app_eq_unit (Eq.symm h')
Proof state after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
h3 : ys = [] ∧ [y] = [x] ∨ ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
h3 : ys = [] ∧ [y] = [x] ∨ ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y
Tactic:
cases h3 with | inl left =>
  cases left with
  | intro empty xy =>
    simp only [cons.injEq, and_true] at xy
    rw [empty, xy]
    apply And.intro <;> rfl
| inr right =>
  cases right with
  | intro empty ysx =>
    contradiction
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case nil.inl
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
left : ys = [] ∧ [y] = [x]
⊢ [] = ys ∧ x = y
Tactic:
cases left with
| intro empty xy =>
  simp only [cons.injEq, and_true] at xy
  rw [empty, xy]
  apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : [y] = [x]
⊢ [] = ys ∧ x = y
Tactic:
simp only [cons.injEq, and_true] at xy
Proof state after:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = ys ∧ x = y
Tactic:
rw [empty, xy]
Proof state after:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = [] ∧ x = x
Theorem: list_app_inj_tail
Proof state before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = [] ∧ x = x
Tactic:
apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case nil.inr
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
right : ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y
Tactic:
cases right with
| intro empty ysx =>
  contradiction
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case nil.inr.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = [x]
ysx : [y] = []
⊢ [] = ys ∧ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
⊢ ∀ {ys : List α}, headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y
Tactic:
intro ys
Proof state after:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
ys : List α
⊢ headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
ys : List α
⊢ headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y
Tactic:
cases ys with
| nil =>
  intro h'
  simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
| cons heady taily =>
  intro h'
  simp only [cons_append, cons.injEq] at h'
  cases h' with
  | intro heads tails =>
    rw [heads]
    have h: tailx = taily ∧ x = y := (ihx tails)
    cases h with
    | intro tailxy xy =>
      rw [tailxy]
      rw [xy]
      apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
⊢ headx :: tailx ++ [x] = [] ++ [y] → headx :: tailx = [] ∧ x = y
Tactic:
intro h'
Proof state after:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
h' : headx :: tailx ++ [x] = [] ++ [y]
⊢ headx :: tailx = [] ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
h' : headx :: tailx ++ [x] = [] ++ [y]
⊢ headx :: tailx = [] ∧ x = y
Tactic:
simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
⊢ headx :: tailx ++ [x] = heady :: taily ++ [y] → headx :: tailx = heady :: taily ∧ x = y
Tactic:
intro h'
Proof state after:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx :: tailx ++ [x] = heady :: taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx :: tailx ++ [x] = heady :: taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
simp only [cons_append, cons.injEq] at h'
Proof state after:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx = heady ∧ tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx = heady ∧ tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
cases h' with
| intro heads tails =>
  rw [heads]
  have h: tailx = taily ∧ x = y := (ihx tails)
  cases h with
  | intro tailxy xy =>
    rw [tailxy]
    rw [xy]
    apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
rw [heads]
Proof state after:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ heady :: tailx = heady :: taily ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
have h: tailx = taily ∧ x = y := (ihx tails)
Proof state after:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
h : tailx = taily ∧ x = y
⊢ heady :: tailx = heady :: taily ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
h : tailx = taily ∧ x = y
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
cases h with
| intro tailxy xy =>
  rw [tailxy]
  rw [xy]
  apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
rw [tailxy]
Proof state after:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ x = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ x = y
Tactic:
rw [xy]
Proof state after:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ y = y
Theorem: list_app_inj_tail
Proof state before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ y = y
Tactic:
apply And.intro <;> rfl
Proof state after:
no goals
Theorem: list_inj_tail_app
Proof state before:
α : Type u_1
xs ys : List α
x y : α
⊢ xs = ys ∧ x = y → xs ++ [x] = ys ++ [y]
Tactic:
intro H
Proof state after:
α : Type u_1
xs ys : List α
x y : α
H : xs = ys ∧ x = y
⊢ xs ++ [x] = ys ++ [y]
Theorem: list_inj_tail_app
Proof state before:
α : Type u_1
xs ys : List α
x y : α
H : xs = ys ∧ x = y
⊢ xs ++ [x] = ys ++ [y]
Tactic:
cases H with
| intro H1 H2 =>
  rw [H1, H2]
Proof state after:
no goals
Theorem: list_inj_tail_app
Proof state before:
case intro
α : Type u_1
xs ys : List α
x y : α
H1 : xs = ys
H2 : x = y
⊢ xs ++ [x] = ys ++ [y]
Tactic:
rw [H1, H2]
Proof state after:
no goals
Theorem: list_app_nil_end
Proof state before:
α : Type u_1
xs : List α
⊢ xs = xs ++ []
Tactic:
cases xs with
| nil => rfl
| cons head tail => simp only [append_nil]
Proof state after:
no goals
Theorem: list_app_nil_end
Proof state before:
case nil
α : Type u_1
⊢ [] = [] ++ []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_nil_end
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
⊢ head :: tail = head :: tail ++ []
Tactic:
simp only [append_nil]
Proof state after:
no goals
Theorem: list_app_length
Proof state before:
α : Type u_1
xs ys : List α
⊢ length (xs ++ ys) = length xs + length ys
Tactic:
cases xs with
| nil => simp only [nil_append, length_nil, zero_add]
| cons _ tailx => simp only [cons_append, length_cons, length_append, succ_add]
Proof state after:
no goals
Theorem: list_app_length
Proof state before:
case nil
α : Type u_1
ys : List α
⊢ length ([] ++ ys) = length [] + length ys
Tactic:
simp only [nil_append, length_nil, zero_add]
Proof state after:
no goals
Theorem: list_app_length
Proof state before:
case cons
α : Type u_1
ys : List α
head✝ : α
tailx : List α
⊢ length (head✝ :: tailx ++ ys) = length (head✝ :: tailx) + length ys
Tactic:
simp only [cons_append, length_cons, length_append, succ_add]
Proof state after:
no goals
Theorem: list_last_length
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ length (xs ++ [x]) = length xs + 1
Tactic:
induction xs with
| nil => rfl
| cons _ tail ih => simp [ih]
Proof state after:
no goals
Theorem: list_last_length
Proof state before:
case nil
α : Type u_1
x : α
⊢ length ([] ++ [x]) = length [] + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: list_last_length
Proof state before:
case cons
α : Type u_1
x head✝ : α
tail : List α
ih : length (tail ++ [x]) = length tail + 1
⊢ length (head✝ :: tail ++ [x]) = length (head✝ :: tail) + 1
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: list_cons_eq
Proof state before:
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys ↔ x = y ∧ xs = ys
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys → x = y ∧ xs = ys

case mpr
α : Type u_1
x y : α
xs ys : List α
⊢ x = y ∧ xs = ys → x :: xs = y :: ys
Theorem: list_cons_eq
Proof state before:
case mp
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys → x = y ∧ xs = ys
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys
Theorem: list_cons_eq
Proof state before:
case mp
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys
Tactic:
apply And.intro
Proof state after:
case mp.left
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y

case mp.right
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ xs = ys
Theorem: list_cons_eq
Proof state before:
case mp.left
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y
Tactic:
injections
Proof state after:
no goals
Theorem: list_cons_eq
Proof state before:
case mp.right
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ xs = ys
Tactic:
injections
Proof state after:
no goals
Theorem: list_cons_eq
Proof state before:
case mpr
α : Type u_1
x y : α
xs ys : List α
⊢ x = y ∧ xs = ys → x :: xs = y :: ys
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x :: xs = y :: ys
Theorem: list_cons_eq
Proof state before:
case mpr
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x :: xs = y :: ys
Tactic:
congr
Proof state after:
case mpr.e_head
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x = y

case mpr.e_tail
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ xs = ys
Theorem: list_cons_eq
Proof state before:
case mpr.e_head
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x = y
Tactic:
exact h.left
Proof state after:
no goals
Theorem: list_cons_eq
Proof state before:
case mpr.e_tail
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ xs = ys
Tactic:
exact h.right
Proof state after:
no goals
Theorem: list_length_zero_or_smaller_is_empty
Proof state before:
α : Type u_1
xs : List α
⊢ length xs ≤ 0 → xs = []
Tactic:
cases xs with
| nil => intro; rfl
| cons head tail => intro; contradiction
Proof state after:
no goals
Theorem: list_length_zero_or_smaller_is_empty
Proof state before:
case nil
α : Type u_1
⊢ length [] ≤ 0 → [] = []
Tactic:
intro
Proof state after:
case nil
α : Type u_1
a✝ : length [] ≤ 0
⊢ [] = []
Theorem: list_length_zero_or_smaller_is_empty
Proof state before:
case nil
α : Type u_1
a✝ : length [] ≤ 0
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_length_zero_or_smaller_is_empty
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
⊢ length (head :: tail) ≤ 0 → head :: tail = []
Tactic:
intro
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
a✝ : length (head :: tail) ≤ 0
⊢ head :: tail = []
Theorem: list_length_zero_or_smaller_is_empty
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
a✝ : length (head :: tail) ≤ 0
⊢ head :: tail = []
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_take_nil
Proof state before:
α : Type u
n : ℕ
⊢ take n [] = []
Tactic:
cases n with
| zero => rfl
| succ => rfl
Proof state after:
no goals
Theorem: list_take_nil
Proof state before:
case zero
α : Type u
⊢ take zero [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_take_nil
Proof state before:
case succ
α : Type u
n✝ : ℕ
⊢ take (succ n✝) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_take_cons
Proof state before:
α : Type u_1
n : ℕ
x : α
xs : List α
⊢ take (n + 1) (x :: xs) = x :: take n xs
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_take_all
Proof state before:
α : Type u_1
xs : List α
⊢ take (length xs) xs = xs
Tactic:
induction xs with
| nil => rfl
| cons head tail ih =>
  have h : take (length (head::tail)) (head::tail) =
      head :: (take (length tail) tail) := by
    apply list_take_cons
  rw [ih] at h
  trivial
Proof state after:
no goals
Theorem: list_take_all
Proof state before:
case nil
α : Type u_1
⊢ take (length []) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_take_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
have h : take (length (head::tail)) (head::tail) =
    head :: (take (length tail) tail) := by
  apply list_take_cons
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Theorem: list_take_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
rw [ih] at h
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Theorem: list_take_all
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
trivial
Proof state after:
no goals
Theorem: list_take_all
Proof state before:
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
⊢ take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
Tactic:
apply list_take_cons
Proof state after:
no goals
Theorem: list_take_zero
Proof state before:
α : Type u_1
xs : List α
⊢ take zero xs = []
Tactic:
rw [take]
Proof state after:
no goals
Theorem: list_rev_empty
Proof state before:
α : Type u_1
xs : List α
⊢ reverse xs = [] → xs = []
Tactic:
cases xs with
| nil => simp only [reverse_nil, forall_true_left]
| cons head tail =>
  intro h
  have h' : (reverse (reverse (head :: tail)) = []) := congrArg reverse h
  simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append] at h'
Proof state after:
no goals
Theorem: list_rev_empty
Proof state before:
case nil
α : Type u_1
⊢ reverse [] = [] → [] = []
Tactic:
simp only [reverse_nil, forall_true_left]
Proof state after:
no goals
Theorem: list_rev_empty
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
⊢ reverse (head :: tail) = [] → head :: tail = []
Tactic:
intro h
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
⊢ head :: tail = []
Theorem: list_rev_empty
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
⊢ head :: tail = []
Tactic:
have h' : (reverse (reverse (head :: tail)) = []) := congrArg reverse h
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
h' : reverse (reverse (head :: tail)) = []
⊢ head :: tail = []
Theorem: list_rev_empty
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
h' : reverse (reverse (head :: tail)) = []
⊢ head :: tail = []
Tactic:
simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append] at h'
Proof state after:
no goals
Theorem: list_rev_empty2
Proof state before:
α : Type u_1
⊢ reverse [] = []
Tactic:
trivial
Proof state after:
no goals
Theorem: list_rev_eq
Proof state before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ reverse xs = reverse ys → xs = ys
Tactic:
intro h
Proof state after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
⊢ xs = ys