internlm/Lean-Github huggingface dataset:
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ (IndView.cons x xs).toList1 = List1.cons y [] ↔ (List1.cons y []).toIndView = IndView.cons x xs
Tactic:
unfold IndView.toList1 toIndView
Proof state after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] ↔ IndView.pure y = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] ↔ IndView.pure y = IndView.cons x xs
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] → IndView.pure y = IndView.cons x xs

case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ IndView.pure y = IndView.cons x xs → List1.cons x xs.toList1.toList = List1.cons y []
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] → IndView.pure y = IndView.cons x xs
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : List1.cons x xs.toList1.toList = List1.cons y []
⊢ IndView.pure y = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : List1.cons x xs.toList1.toList = List1.cons y []
⊢ IndView.pure y = IndView.cons x xs
Tactic:
injection h with h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : x :: xs.toList1.toList = [y]
⊢ IndView.pure y = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : x :: xs.toList1.toList = [y]
⊢ IndView.pure y = IndView.cons x xs
Tactic:
injection h with hh ht
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ IndView.pure y = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ IndView.pure y = IndView.cons x xs
Tactic:
absurd ht
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ ¬xs.toList1.toList = []
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ ¬xs.toList1.toList = []
Tactic:
exact List1.ne_nil xs.toList1
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ IndView.pure y = IndView.cons x xs → List1.cons x xs.toList1.toList = List1.cons y []
Tactic:
intro
Proof state after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
a✝ : IndView.pure y = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y []
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
a✝ : IndView.pure y = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y []
Tactic:
contradiction
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ (IndView.cons x xs).toList1 = List1.cons y (head✝ :: tail✝) ↔
    (List1.cons y (head✝ :: tail✝)).toIndView = IndView.cons x xs
Tactic:
unfold IndView.toList1 toIndView
Proof state after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (head✝ :: tail✝) ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (head✝ :: tail✝) ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
rw [←cons_toList]
Proof state after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList →
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs →
    List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList →
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
injection h with h
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : x :: xs.toList1.toList = y :: (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : x :: xs.toList1.toList = y :: (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
injection h with hh ht
Proof state after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : x = y
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : x = y
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
cases hh
Proof state after:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
have ht := List1.eq ht
Proof state after:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
congr
Proof state after:
case mp.refl.e_a
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ (List1.cons head✝ tail✝).toIndView = xs
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mp.refl.e_a
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ (List1.cons head✝ tail✝).toIndView = xs
Tactic:
exact toList1_eq_iff_toIndView_eq.mp ht
Proof state after:
no goals
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs →
    List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
injection h with hh ht
Proof state after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : y = x
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : y = x
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
cases hh
Proof state after:
case mpr.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons x (List1.cons head✝ tail✝).toList
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons x (List1.cons head✝ tail✝).toList
Tactic:
congr
Proof state after:
case mpr.refl.e_xs.e_self
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ xs.toList1 = List1.cons head✝ tail✝
Theorem: List1.toList1_eq_iff_toIndView_eq
Proof state before:
case mpr.refl.e_xs.e_self
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ xs.toList1 = List1.cons head✝ tail✝
Tactic:
exact toList1_eq_iff_toIndView_eq.mpr ht
Proof state after:
no goals
Theorem: List1.IndView.sizeOf_toList1
Proof state before:
α : Type u_1
β : Type ?u.12658
xs : List1.IndView α
⊢ sizeOf xs.toList1 = 2 + sizeOf xs
Tactic:
induction xs with
| pure x => rw [toList1]; rfl
| cons x xs ih => rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]; rfl
Proof state after:
no goals
Theorem: List1.IndView.sizeOf_toList1
Proof state before:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (pure x).toList1 = 2 + sizeOf (pure x)
Tactic:
rw [toList1]
Proof state after:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (List1.cons x []) = 2 + sizeOf (pure x)
Theorem: List1.IndView.sizeOf_toList1
Proof state before:
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (List1.cons x []) = 2 + sizeOf (pure x)
Tactic:
rfl
Proof state after:
no goals
Theorem: List1.IndView.sizeOf_toList1
Proof state before:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ sizeOf (cons x xs).toList1 = 2 + sizeOf (cons x xs)
Tactic:
rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]
Proof state after:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ 2 + (1 + sizeOf xs) = 2 + sizeOf (cons x xs)
Theorem: List1.IndView.sizeOf_toList1
Proof state before:
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ 2 + (1 + sizeOf xs) = 2 + sizeOf (cons x xs)
Tactic:
rfl
Proof state after:
no goals
Theorem: List1.append_compat_left
Proof state before:
α : Type u_1
β : Type ?u.22157
xs✝ ys : List1 α
zs : List α
x : α
xs : List α
⊢ xs ++ ys.toList ++ zs = xs ++ (ys.append zs).toList
Tactic:
rw [append_toList_left, List.append_assoc]
Proof state after:
no goals
Theorem: Nat.succ_pred'
Proof state before:
x : Nat
h : autoParam (x > 0) _auto✝
⊢ x - 1 + 1 = x
Tactic:
cases x with
| zero => contradiction
| succ x => rfl
Proof state after:
no goals
Theorem: Nat.succ_pred'
Proof state before:
case zero
h : autoParam (0 > 0) _auto✝
⊢ 0 - 1 + 1 = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.succ_pred'
Proof state before:
case succ
x : Nat
h : autoParam (x + 1 > 0) _auto✝
⊢ x + 1 - 1 + 1 = x + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case zero_left
x : Nat
⊢ 0 + 1 ≤ x ∨ 0 = 0 ↔ 0 ≤ x - 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case zero_right
y : Nat
⊢ y + 1 ≤ 0 ∨ y = 0 ↔ y ≤ 0 - 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case succ_succ
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 ↔ x + 1 ≤ y + 1 - 1
Tactic:
constructor
Proof state after:
case succ_succ.mp
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 → x + 1 ≤ y + 1 - 1

case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 ≤ y + 1 - 1 → x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case succ_succ.mp
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 → x + 1 ≤ y + 1 - 1
Tactic:
intro
| Or.inl h => exact Nat.le_of_succ_le_succ h
| Or.inr h => absurd h; apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 + 1 ≤ y + 1
⊢ x + 1 ≤ y + 1 - 1
Tactic:
exact Nat.le_of_succ_le_succ h
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ x + 1 ≤ y + 1 - 1
Tactic:
absurd h
Proof state after:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Tactic:
apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 ≤ y + 1 - 1 → x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Tactic:
intro h
Proof state after:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Tactic:
left
Proof state after:
case succ_succ.mpr.h
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1
Theorem: Nat.succ_le_or_eq_zero_iff_le_pred
Proof state before:
case succ_succ.mpr.h
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1
Tactic:
exact Nat.succ_le_succ h
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_left
x : Nat
⊢ 0 - 1 < x ∨ 0 = 0 ↔ 0 < x + 1
Tactic:
simp [Nat.zero_lt_succ]
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right
y : Nat
⊢ y - 1 < 0 ∨ y = 0 ↔ y < 0 + 1
Tactic:
constructor
Proof state after:
case zero_right.mp
y : Nat
⊢ y - 1 < 0 ∨ y = 0 → y < 0 + 1

case zero_right.mpr
y : Nat
⊢ y < 0 + 1 → y - 1 < 0 ∨ y = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mp
y : Nat
⊢ y - 1 < 0 ∨ y = 0 → y < 0 + 1
Tactic:
simp [Nat.not_lt_zero]
Proof state after:
case zero_right.mp
y : Nat
⊢ y = 0 → y < 1
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mp
y : Nat
⊢ y = 0 → y < 1
Tactic:
intro h
Proof state after:
case zero_right.mp
y : Nat
h : y = 0
⊢ y < 1
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mp
y : Nat
h : y = 0
⊢ y < 1
Tactic:
rw [h]
Proof state after:
case zero_right.mp
y : Nat
h : y = 0
⊢ 0 < 1
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mp
y : Nat
h : y = 0
⊢ 0 < 1
Tactic:
exact Nat.zero_lt_one
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mpr
y : Nat
⊢ y < 0 + 1 → y - 1 < 0 ∨ y = 0
Tactic:
simp [Nat.not_lt_zero]
Proof state after:
case zero_right.mpr
y : Nat
⊢ y < 1 → y = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mpr
y : Nat
⊢ y < 1 → y = 0
Tactic:
intro h
Proof state after:
case zero_right.mpr
y : Nat
h : y < 1
⊢ y = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case zero_right.mpr
y : Nat
h : y < 1
⊢ y = 0
Tactic:
exact Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ h)
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case succ_succ
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 ↔ x + 1 < y + 1 + 1
Tactic:
constructor
Proof state after:
case succ_succ.mp
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 → x + 1 < y + 1 + 1

case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 < y + 1 + 1 → x + 1 - 1 < y + 1 ∨ x + 1 = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case succ_succ.mp
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0 → x + 1 < y + 1 + 1
Tactic:
intro
| Or.inl h => exact Nat.succ_lt_succ h
| Or.inr h => absurd h; apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 - 1 < y + 1
⊢ x + 1 < y + 1 + 1
Tactic:
exact Nat.succ_lt_succ h
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ x + 1 < y + 1 + 1
Tactic:
absurd h
Proof state after:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
x✝ : x + 1 - 1 < y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Tactic:
apply Nat.succ_ne_zero
Proof state after:
no goals
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
⊢ x + 1 < y + 1 + 1 → x + 1 - 1 < y + 1 ∨ x + 1 = 0
Tactic:
intro h
Proof state after:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case succ_succ.mpr
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1 ∨ x + 1 = 0
Tactic:
left
Proof state after:
case succ_succ.mpr.h
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1
Theorem: Nat.pred_lt_or_eq_zero_iff_lt_succ
Proof state before:
case succ_succ.mpr.h
x y : Nat
a✝ : x - 1 < y ∨ x = 0 ↔ x < y + 1
h : x + 1 < y + 1 + 1
⊢ x + 1 - 1 < y + 1
Tactic:
exact Nat.lt_of_succ_lt_succ h
Proof state after:
no goals
Theorem: Ordering.opp_opp
Proof state before:
x : Ordering
⊢ x.opp.opp = x
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: Ordering.opp_inj
Proof state before:
x y : Ordering
⊢ x.opp = y.opp → x = y
Tactic:
intro h
Proof state after:
x y : Ordering
h : x.opp = y.opp
⊢ x = y
Theorem: Ordering.opp_inj
Proof state before:
x y : Ordering
h : x.opp = y.opp
⊢ x = y
Tactic:
rw [←opp_opp x, ←opp_opp y, h]
Proof state after:
no goals
Theorem: Ordering.eq_opp_iff_opp_eq
Proof state before:
x y : Ordering
⊢ x.opp = y ↔ x = y.opp
Tactic:
constructor
Proof state after:
case mp
x y : Ordering
⊢ x.opp = y → x = y.opp

case mpr
x y : Ordering
⊢ x = y.opp → x.opp = y
Theorem: Ordering.eq_opp_iff_opp_eq
Proof state before:
case mp
x y : Ordering
⊢ x.opp = y → x = y.opp
Tactic:
intro h
Proof state after:
case mp
x y : Ordering
h : x.opp = y
⊢ x = y.opp
Theorem: Ordering.eq_opp_iff_opp_eq
Proof state before:
case mp
x y : Ordering
h : x.opp = y
⊢ x = y.opp
Tactic:
rw [←h, opp_opp]
Proof state after:
no goals
Theorem: Ordering.eq_opp_iff_opp_eq
Proof state before:
case mpr
x y : Ordering
⊢ x = y.opp → x.opp = y
Tactic:
intro h
Proof state after:
case mpr
x y : Ordering
h : x = y.opp
⊢ x.opp = y
Theorem: Ordering.eq_opp_iff_opp_eq
Proof state before:
case mpr
x y : Ordering
h : x = y.opp
⊢ x.opp = y
Tactic:
rw [h, opp_opp]
Proof state after:
no goals