internlm/Lean-Github huggingface dataset:
Theorem: Eq.all_tequal
Proof state before:
case refl
α✝ : Sort u_1
x : α✝
q : x = x
⊢ (_ : x = x) = q
Tactic:
cases q
Proof state after:
case refl.refl
α✝ : Sort u_1
x : α✝
⊢ (_ : x = x) = (_ : x = x)
Theorem: Eq.all_tequal
Proof state before:
case refl.refl
α✝ : Sort u_1
x : α✝
⊢ (_ : x = x) = (_ : x = x)
Tactic:
apply refl
Proof state after:
no goals
Theorem: TEq.all_tequal
Proof state before:
α✝ : Type u_1
x y : α✝
p q : x ≡ y
⊢ p ≡ q
Tactic:
cases p
Proof state after:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x ≡ q
Theorem: TEq.all_tequal
Proof state before:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x ≡ q
Tactic:
cases q
Proof state after:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x ≡ refl x
Theorem: TEq.all_tequal
Proof state before:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x ≡ refl x
Tactic:
apply refl
Proof state after:
no goals
Theorem: TEq.all_equal
Proof state before:
α✝ : Type u_1
x y : α✝
p q : x ≡ y
⊢ p = q
Tactic:
cases p
Proof state after:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x = q
Theorem: TEq.all_equal
Proof state before:
case refl
α✝ : Type u_1
x : α✝
q : x ≡ x
⊢ refl x = q
Tactic:
cases q
Proof state after:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x = refl x
Theorem: TEq.all_equal
Proof state before:
case refl.refl
α✝ : Type u_1
x : α✝
⊢ refl x = refl x
Tactic:
rfl
Proof state after:
no goals
Theorem: t
Proof state before:
⊢ 1 ≡ 2 → False
Tactic:
intro x
Proof state after:
x : 1 ≡ 2
⊢ False
Theorem: t
Proof state before:
x : 1 ≡ 2
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: t''
Proof state before:
⊢ 1 = 2 → False
Tactic:
intro
Proof state after:
a✝ : 1 = 2
⊢ False
Theorem: t''
Proof state before:
a✝ : 1 = 2
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: nat_succ_le_succ_iff
Proof state before:
x y : ℕ
⊢ succ x ≤ succ y ↔ x ≤ y
Tactic:
apply Iff.intro
Proof state after:
case mp
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y

case mpr
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y
Theorem: nat_succ_le_succ_iff
Proof state before:
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y
Tactic:
case mp =>
  apply Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: nat_succ_le_succ_iff
Proof state before:
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y
Tactic:
case mpr =>
  apply Nat.succ_le_succ
Proof state after:
no goals
Theorem: nat_succ_le_succ_iff
Proof state before:
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: nat_succ_le_succ_iff
Proof state before:
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y
Tactic:
apply Nat.succ_le_succ
Proof state after:
no goals
Theorem: nat_succ_eq_plus_one
Proof state before:
n : ℕ
⊢ succ n = n + 1
Tactic:
simp only
Proof state after:
no goals
Theorem: nat_pred_le_succ'
Proof state before:
⊢ ∀ {n m : ℕ}, Nat.le n (succ m) → Nat.le (pred n) m
Tactic:
intro n m h
Proof state after:
n m : ℕ
h : Nat.le n (succ m)
⊢ Nat.le (pred n) m
Theorem: nat_pred_le_succ'
Proof state before:
n m : ℕ
h : Nat.le n (succ m)
⊢ Nat.le (pred n) m
Tactic:
cases h with
| refl =>
  constructor
| step h =>
  cases n with
  | zero =>
    dsimp only [zero_eq, Nat.pred_zero, le_eq]
    exact h
  | succ n =>
    dsimp only [Nat.pred_succ, le_eq]
    have h_n_le_succ_n := Nat.le_succ n
    exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: nat_pred_le_succ'
Proof state before:
case refl
m : ℕ
⊢ Nat.le (pred (succ m)) m
Tactic:
constructor
Proof state after:
no goals
Theorem: nat_pred_le_succ'
Proof state before:
case step
n m : ℕ
h : Nat.le n m
⊢ Nat.le (pred n) m
Tactic:
cases n with
| zero =>
  dsimp only [zero_eq, Nat.pred_zero, le_eq]
  exact h
| succ n =>
  dsimp only [Nat.pred_succ, le_eq]
  have h_n_le_succ_n := Nat.le_succ n
  exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: nat_pred_le_succ'
Proof state before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ Nat.le (pred zero) m
Tactic:
dsimp only [zero_eq, Nat.pred_zero, le_eq]
Proof state after:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m
Theorem: nat_pred_le_succ'
Proof state before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m
Tactic:
exact h
Proof state after:
no goals
Theorem: nat_pred_le_succ'
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ Nat.le (pred (succ n)) m
Tactic:
dsimp only [Nat.pred_succ, le_eq]
Proof state after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m
Theorem: nat_pred_le_succ'
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m
Tactic:
have h_n_le_succ_n := Nat.le_succ n
Proof state after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m
Theorem: nat_pred_le_succ'
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m
Tactic:
exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: nat_min_zero
Proof state before:
n : ℕ
⊢ min 0 n = 0
Tactic:
unfold min
Proof state after:
n : ℕ
⊢ instMinNat.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : ℕ
⊢ instMinNat.1 0 n = 0
Tactic:
unfold instMinNat
Proof state after:
n : ℕ
⊢ minOfLe.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : ℕ
⊢ minOfLe.1 0 n = 0
Tactic:
unfold minOfLe
Proof state after:
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 0 n = 0
Theorem: nat_min_zero
Proof state before:
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 0 n = 0
Tactic:
simp
Proof state after:
no goals
Theorem: nat_zero_min
Proof state before:
n : ℕ
⊢ min n 0 = 0
Tactic:
cases n with
| zero =>
  simp
| succ n =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [nonpos_iff_eq_zero, ite_false]
Proof state after:
no goals
Theorem: nat_zero_min
Proof state before:
case zero

⊢ min zero 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: nat_zero_min
Proof state before:
case succ
n : ℕ
⊢ min (succ n) 0 = 0
Tactic:
unfold min
Proof state after:
case succ
n : ℕ
⊢ instMinNat.1 (succ n) 0 = 0
Theorem: nat_zero_min
Proof state before:
case succ
n : ℕ
⊢ instMinNat.1 (succ n) 0 = 0
Tactic:
unfold instMinNat
Proof state after:
case succ
n : ℕ
⊢ minOfLe.1 (succ n) 0 = 0
Theorem: nat_zero_min
Proof state before:
case succ
n : ℕ
⊢ minOfLe.1 (succ n) 0 = 0
Tactic:
unfold minOfLe
Proof state after:
case succ
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 (succ n) 0 = 0
Theorem: nat_zero_min
Proof state before:
case succ
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 (succ n) 0 = 0
Tactic:
simp only [nonpos_iff_eq_zero, ite_false]
Proof state after:
no goals
Theorem: nat_add_succ_is_succ_add
Proof state before:
n m : ℕ
⊢ succ n + m = succ (n + m)
Tactic:
cases n with
| zero =>
  rewrite [Nat.add_comm]
  simp only [zero_eq, zero_add]
| succ n =>
  rewrite [Nat.add_comm]
  rewrite [Nat.add_comm (succ n)]
  repeat rewrite [Nat.add_succ]
  rfl
Proof state after:
no goals
Theorem: nat_add_succ_is_succ_add
Proof state before:
case zero
m : ℕ
⊢ succ zero + m = succ (zero + m)
Tactic:
rewrite [Nat.add_comm]
Proof state after:
case zero
m : ℕ
⊢ m + succ zero = succ (zero + m)
Theorem: nat_add_succ_is_succ_add
Proof state before:
case zero
m : ℕ
⊢ m + succ zero = succ (zero + m)
Tactic:
simp only [zero_eq, zero_add]
Proof state after:
no goals
Theorem: nat_add_succ_is_succ_add
Proof state before:
case succ
m n : ℕ
⊢ succ (succ n) + m = succ (succ n + m)
Tactic:
rewrite [Nat.add_comm]
Proof state after:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (succ n + m)
Theorem: nat_add_succ_is_succ_add
Proof state before:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (succ n + m)
Tactic:
rewrite [Nat.add_comm (succ n)]
Proof state after:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (m + succ n)
Theorem: nat_add_succ_is_succ_add
Proof state before:
case succ
m n : ℕ
⊢ m + succ (succ n) = succ (m + succ n)
Tactic:
repeat rewrite [Nat.add_succ]
Proof state after:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))
Theorem: nat_add_succ_is_succ_add
Proof state before:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))
Tactic:
rfl
Proof state after:
no goals
Theorem: nat_add_succ_is_succ_add
Proof state before:
case succ
m n : ℕ
⊢ succ (m + (n + 1)) = succ (m + succ n)
Tactic:
rewrite [Nat.add_succ]
Proof state after:
case succ
m n : ℕ
⊢ succ (succ (m + n)) = succ (succ (m + n))
Theorem: nat_pred_le_pred
Proof state before:
⊢ ∀ {n m : ℕ}, n ≤ m → pred n ≤ pred m
Tactic:
intro n m h
Proof state after:
n m : ℕ
h : n ≤ m
⊢ pred n ≤ pred m
Theorem: nat_pred_le_pred
Proof state before:
n m : ℕ
h : n ≤ m
⊢ pred n ≤ pred m
Tactic:
cases h with
| refl => constructor
| step h =>
  rename_i m
  cases n with
  | zero =>
    dsimp
    exact h
  | succ n =>
    dsimp
    have h_n_le_succ_n := Nat.le_succ n
    exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: nat_pred_le_pred
Proof state before:
case refl
n : ℕ
⊢ pred n ≤ pred n
Tactic:
constructor
Proof state after:
no goals
Theorem: nat_pred_le_pred
Proof state before:
case step
n m✝ : ℕ
h : Nat.le n m✝
⊢ pred n ≤ pred (succ m✝)
Tactic:
rename_i m
Proof state after:
case step
n m : ℕ
h : Nat.le n m
⊢ pred n ≤ pred (succ m)
Theorem: nat_pred_le_pred
Proof state before:
case step
n m : ℕ
h : Nat.le n m
⊢ pred n ≤ pred (succ m)
Tactic:
cases n with
| zero =>
  dsimp
  exact h
| succ n =>
  dsimp
  have h_n_le_succ_n := Nat.le_succ n
  exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: nat_pred_le_pred
Proof state before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ pred zero ≤ pred (succ m)
Tactic:
dsimp
Proof state after:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m
Theorem: nat_pred_le_pred
Proof state before:
case step.zero
m : ℕ
h : Nat.le zero m
⊢ 0 ≤ m
Tactic:
exact h
Proof state after:
no goals
Theorem: nat_pred_le_pred
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ pred (succ n) ≤ pred (succ m)
Tactic:
dsimp
Proof state after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m
Theorem: nat_pred_le_pred
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
⊢ n ≤ m
Tactic:
have h_n_le_succ_n := Nat.le_succ n
Proof state after:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m
Theorem: nat_pred_le_pred
Proof state before:
case step.succ
m n : ℕ
h : Nat.le (succ n) m
h_n_le_succ_n : n ≤ succ n
⊢ n ≤ m
Tactic:
exact (Nat.le_trans h_n_le_succ_n h)
Proof state after:
no goals
Theorem: list_cons_ne_nil
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ x :: xs ≠ []
Tactic:
intro h'
Proof state after:
α : Type u_1
x : α
xs : List α
h' : x :: xs = []
⊢ False
Theorem: list_cons_ne_nil
Proof state before:
α : Type u_1
x : α
xs : List α
h' : x :: xs = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_cons_nil_ne
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ [] ≠ x :: xs
Tactic:
intro h'
Proof state after:
α : Type u_1
x : α
xs : List α
h' : [] = x :: xs
⊢ False
Theorem: list_cons_nil_ne
Proof state before:
α : Type u_1
x : α
xs : List α
h' : [] = x :: xs
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_append_ne_nil
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ [x] ++ xs ≠ []
Tactic:
intro h'
Proof state after:
α : Type u_1
x : α
xs : List α
h' : [x] ++ xs = []
⊢ False
Theorem: list_append_ne_nil
Proof state before:
α : Type u_1
x : α
xs : List α
h' : [x] ++ xs = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_append_nil_ne
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ xs ++ [x] ≠ []
Tactic:
intro h'
Proof state after:
α : Type u_1
x : α
xs : List α
h' : xs ++ [x] = []
⊢ False
Theorem: list_append_nil_ne
Proof state before:
α : Type u_1
x : α
xs : List α
h' : xs ++ [x] = []
⊢ False
Tactic:
cases xs with
| nil =>
  contradiction
| cons head tail =>
  contradiction
Proof state after:
no goals
Theorem: list_append_nil_ne
Proof state before:
case nil
α : Type u_1
x : α
h' : [] ++ [x] = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_append_nil_ne
Proof state before:
case cons
α : Type u_1
x head : α
tail : List α
h' : head :: tail ++ [x] = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_length_zero_is_empty
Proof state before:
α : Type u_1
xs : List α
⊢ length xs = 0 → xs = []
Tactic:
cases xs
Proof state after:
case nil
α : Type u_1
⊢ length [] = 0 → [] = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ length (head✝ :: tail✝) = 0 → head✝ :: tail✝ = []
Theorem: list_length_zero_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_is_empty
Proof state before:
case nil
α : Type u_1
a✝ : length [] = 0
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_length_zero_is_empty
Proof state before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ length (head✝ :: tail✝) = 0 → head✝ :: tail✝ = []
Tactic:
intro h'
Proof state after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h' : length (head✝ :: tail✝) = 0
⊢ head✝ :: tail✝ = []
Theorem: list_length_zero_is_empty
Proof state before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h' : length (head✝ :: tail✝) = 0
⊢ head✝ :: tail✝ = []
Tactic:
simp only [length, add_eq_zero_iff, and_false] at h'
Proof state after:
no goals
Theorem: list_app_nil_l
Proof state before:
α : Type u_1
xs : List α
⊢ [] ++ xs = xs
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_nil_r
Proof state before:
α : Type u_1
xs : List α
⊢ xs ++ [] = xs
Tactic:
induction xs with
| nil =>
  rfl
| cons head tail ih =>
  apply (congrArg (cons head))
  assumption
Proof state after:
no goals
Theorem: list_app_nil_r
Proof state before:
case nil
α : Type u_1
⊢ [] ++ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_nil_r
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : tail ++ [] = tail
⊢ head :: tail ++ [] = head :: tail
Tactic:
apply (congrArg (cons head))
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : tail ++ [] = tail
⊢ List.append tail [] = tail
Theorem: list_app_nil_r
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : tail ++ [] = tail
⊢ List.append tail [] = tail
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_assoc
Proof state before:
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs
Tactic:
induction xs with
| nil => rfl
| cons head tail ih =>
  apply (congrArg (cons head))
  exact ih
Proof state after:
no goals
Theorem: list_app_assoc
Proof state before:
case nil
α : Type u_1
ys zs : List α
⊢ [] ++ (ys ++ zs) = [] ++ ys ++ zs
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_assoc
Proof state before:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ head :: tail ++ (ys ++ zs) = head :: tail ++ ys ++ zs
Tactic:
apply (congrArg (cons head))
Proof state after:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ List.append tail (ys ++ zs) = List.append (List.append tail ys) zs
Theorem: list_app_assoc
Proof state before:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ List.append tail (ys ++ zs) = List.append (List.append tail ys) zs
Tactic:
exact ih
Proof state after:
no goals
Theorem: list_app_assoc_singleton
Proof state before:
α : Type u_1
xs ys : List α
z : α
⊢ xs ++ (ys ++ [z]) = xs ++ ys ++ [z]
Tactic:
apply list_app_assoc
Proof state after:
no goals
Theorem: list_app_assoc_reverse
Proof state before:
α : Type u_1
xs ys zs : List α
⊢ xs ++ ys ++ zs = xs ++ (ys ++ zs)
Tactic:
apply Eq.symm
Proof state after:
case h
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs
Theorem: list_app_assoc_reverse
Proof state before:
case h
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs
Tactic:
apply list_app_assoc
Proof state after:
no goals
Theorem: list_app_comm_cons
Proof state before:
α : Type u_1
x : α
xs ys : List α
⊢ x :: (xs ++ ys) = x :: xs ++ ys
Tactic:
apply (congrArg (cons x))
Proof state after:
α : Type u_1
x : α
xs ys : List α
⊢ xs ++ ys = List.append xs ys
Theorem: list_app_comm_cons
Proof state before:
α : Type u_1
x : α
xs ys : List α
⊢ xs ++ ys = List.append xs ys
Tactic:
rfl
Proof state after:
no goals
Theorem: list_nil_ne_app_cons
Proof state before:
α : Type u_1
y : α
xs ys : List α
⊢ [] ≠ xs ++ y :: ys
Tactic:
cases xs <;> { intro h' ; contradiction }
Proof state after:
no goals
Theorem: list_nil_ne_app_cons
Proof state before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
⊢ [] ≠ head✝ :: tail✝ ++ y :: ys
Tactic:
intro h'
Proof state after:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : [] = head✝ :: tail✝ ++ y :: ys
⊢ False
Theorem: list_nil_ne_app_cons
Proof state before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : [] = head✝ :: tail✝ ++ y :: ys
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_app_cons_ne_nil
Proof state before:
α : Type u_1
y : α
xs ys : List α
⊢ xs ++ y :: ys ≠ []
Tactic:
cases xs <;> { intro h' ; contradiction }
Proof state after:
no goals
Theorem: list_app_cons_ne_nil
Proof state before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ y :: ys ≠ []
Tactic:
intro h'
Proof state after:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : head✝ :: tail✝ ++ y :: ys = []
⊢ False
Theorem: list_app_cons_ne_nil
Proof state before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : head✝ :: tail✝ ++ y :: ys = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] ↔ xs = [] ∧ ys = []
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []

case mpr
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []
Tactic:
case mp =>
  cases xs with
  | nil =>
    simp only [nil_append, true_and, imp_self]
  | cons head tail =>
    intro h'
    contradiction
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []
Tactic:
case mpr =>
  intro h'
  cases h' with
  | intro h1 h2 =>
    rw [h1, h2]
    rfl
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
⊢ xs ++ ys = [] → xs = [] ∧ ys = []
Tactic:
cases xs with
| nil =>
  simp only [nil_append, true_and, imp_self]
| cons head tail =>
  intro h'
  contradiction
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
case nil
α : Type u_1
ys : List α
⊢ [] ++ ys = [] → [] = [] ∧ ys = []
Tactic:
simp only [nil_append, true_and, imp_self]
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
⊢ head :: tail ++ ys = [] → head :: tail = [] ∧ ys = []
Tactic:
intro h'
Proof state after:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
h' : head :: tail ++ ys = []
⊢ head :: tail = [] ∧ ys = []
Theorem: list_app_nil_nil
Proof state before:
case cons
α : Type u_1
ys : List α
head : α
tail : List α
h' : head :: tail ++ ys = []
⊢ head :: tail = [] ∧ ys = []
Tactic:
contradiction
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
⊢ xs = [] ∧ ys = [] → xs ++ ys = []
Tactic:
intro h'
Proof state after:
α : Type u_1
xs ys : List α
h' : xs = [] ∧ ys = []
⊢ xs ++ ys = []
Theorem: list_app_nil_nil
Proof state before:
α : Type u_1
xs ys : List α
h' : xs = [] ∧ ys = []
⊢ xs ++ ys = []
Tactic:
cases h' with
| intro h1 h2 =>
  rw [h1, h2]
  rfl
Proof state after:
no goals
Theorem: list_app_nil_nil
Proof state before:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ xs ++ ys = []
Tactic:
rw [h1, h2]
Proof state after:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ [] ++ [] = []
Theorem: list_app_nil_nil
Proof state before:
case intro
α : Type u_1
xs ys : List α
h1 : xs = []
h2 : ys = []
⊢ [] ++ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
α : Type u_1
a : α
xs ys : List α
⊢ xs ++ ys = [a] → xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
cases xs with
| nil =>
  intro hy
  simp only [nil_append] at hy
  apply Or.intro_left
  apply And.intro
  case left => rfl
  case right => assumption
| cons head tail =>
  intro hy
  simp only [cons_append, cons.injEq, append_eq_nil] at hy
  apply Or.intro_right
  cases hy with
  | intro h1 h2 =>
    rw [h1]
    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 nil
α : Type u_1
a : α
ys : List α
⊢ [] ++ ys = [a] → [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Tactic:
intro hy
Proof state after:
case nil
α : Type u_1
a : α
ys : List α
hy : [] ++ ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case nil
α : Type u_1
a : α
ys : List α
hy : [] ++ ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Tactic:
simp only [nil_append] at hy
Proof state after:
case nil
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case nil
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Tactic:
apply Or.intro_left
Proof state after:
case nil.h
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a]
Theorem: list_app_eq_unit
Proof state before:
case nil.h
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a]
Tactic:
apply And.intro
Proof state after:
case nil.h.left
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []

case nil.h.right
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]
Theorem: list_app_eq_unit
Proof state before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []
Tactic:
case left => rfl
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]
Tactic:
case right => assumption
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]
Tactic:
assumption
Proof state after:
no goals
Theorem: list_app_eq_unit
Proof state before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
⊢ head :: tail ++ ys = [a] → head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
intro hy
Proof state after:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head :: tail ++ ys = [a]
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head :: tail ++ ys = [a]
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
simp only [cons_append, cons.injEq, append_eq_nil] at hy
Proof state after:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
apply Or.intro_right
Proof state after:
case cons.h
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []
Theorem: list_app_eq_unit
Proof state before:
case cons.h
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []
Tactic:
cases hy with
| intro h1 h2 =>
  rw [h1]
  cases h2 with
  | intro h4 h5 =>
    rw [h4, h5]
    apply And.intro <;> rfl
Proof state after:
no goals