internlm/Lean-Github huggingface dataset:
Theorem: MyNat.one_add_le_self
Proof state before:
x : Nat
⊢ x ≤ x + one
Tactic:
exists one
Proof state after:
no goals
Theorem: MyNat.le_refl
Proof state before:
x : Nat
⊢ x ≤ x
Tactic:
exists zero
Proof state after:
no goals
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
⊢ a ≤ b → a ≤ succ b
Tactic:
intro
| ⟨ c, hc ⟩ =>
  exists succ c
  repeat (rw [succ_eq_add_one])
  rw [← add_assoc, hc]
Proof state after:
no goals
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ a ≤ succ b
Tactic:
exists succ c
Proof state after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ succ b = a + succ c
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ succ b = a + succ c
Tactic:
repeat (rw [succ_eq_add_one])
Proof state after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)
Tactic:
rw [← add_assoc, hc]
Proof state after:
no goals
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + succ c
Tactic:
(rw [succ_eq_add_one])
Proof state after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)
Theorem: MyNat.le_succ
Proof state before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + succ c
Tactic:
rw [succ_eq_add_one]
Proof state after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)
Theorem: MyNat.zero_le
Proof state before:
a : Nat
⊢ zero ≤ a
Tactic:
exists a
Proof state after:
a : Nat
⊢ a = zero + a
Theorem: MyNat.zero_le
Proof state before:
a : Nat
⊢ a = zero + a
Tactic:
rw [zero_add]
Proof state after:
no goals
Theorem: MyNat.le_trans
Proof state before:
a b c : Nat
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
Tactic:
cases hab with
| intro d hd =>
  cases hbc with
  | intro e he =>
    exists d + e
    rw [he, hd]
    simp
Proof state after:
no goals
Theorem: MyNat.le_trans
Proof state before:
case intro
a b c : Nat
hbc : b ≤ c
d : Nat
hd : b = a + d
⊢ a ≤ c
Tactic:
cases hbc with
| intro e he =>
  exists d + e
  rw [he, hd]
  simp
Proof state after:
no goals
Theorem: MyNat.le_trans
Proof state before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a ≤ c
Tactic:
exists d + e
Proof state after:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ c = a + (d + e)
Theorem: MyNat.le_trans
Proof state before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ c = a + (d + e)
Tactic:
rw [he, hd]
Proof state after:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a + d + e = a + (d + e)
Theorem: MyNat.le_trans
Proof state before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a + d + e = a + (d + e)
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.le_antisymm
Proof state before:
a b : Nat
hab : a ≤ b
hba : b ≤ a
⊢ a = b
Tactic:
cases hab with
| intro w hw =>
  cases hba with
    | intro z hz =>
      rw [hz] at hw
      have hw1 : b + z + w = b := Eq.symm hw
      rw [add_assoc] at hw1
      have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
      have hzz : z = 0 := add_right_eq_zero hzw
      rw [hzz] at hz
      assumption
Proof state after:
no goals
Theorem: MyNat.le_antisymm
Proof state before:
case intro
a b : Nat
hba : b ≤ a
w : Nat
hw : b = a + w
⊢ a = b
Tactic:
cases hba with
  | intro z hz =>
    rw [hz] at hw
    have hw1 : b + z + w = b := Eq.symm hw
    rw [add_assoc] at hw1
    have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
    have hzz : z = 0 := add_right_eq_zero hzw
    rw [hzz] at hz
    assumption
Proof state after:
no goals
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w : Nat
hw : b = a + w
z : Nat
hz : a = b + z
⊢ a = b
Tactic:
rw [hz] at hw
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
⊢ a = b
Tactic:
have hw1 : b + z + w = b := Eq.symm hw
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + z + w = b
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + z + w = b
⊢ a = b
Tactic:
rw [add_assoc] at hw1
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
⊢ a = b
Tactic:
have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
⊢ a = b
Tactic:
have hzz : z = 0 := add_right_eq_zero hzw
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + z
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Tactic:
rw [hzz] at hz
Proof state after:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + 0
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Theorem: MyNat.le_antisymm
Proof state before:
case intro.intro
a b w z : Nat
hw : b = b + z + w
hz : a = b + 0
hw1 : b + (z + w) = b
hzw : z + w = 0
hzz : z = 0
⊢ a = b
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.le_zero
Proof state before:
a : Nat
h : a ≤ zero
⊢ a = 0
Tactic:
cases h with
| intro w pw =>
  exact add_right_eq_zero (Eq.symm pw)
Proof state after:
no goals
Theorem: MyNat.le_zero
Proof state before:
case intro
a w : Nat
pw : zero = a + w
⊢ a = 0
Tactic:
exact add_right_eq_zero (Eq.symm pw)
Proof state after:
no goals
Theorem: MyNat.succ_le_succ
Proof state before:
a b : Nat
h : a ≤ b
⊢ succ a ≤ succ b
Tactic:
cases h with
| intro w pw =>
  exists w
  rw [succ_add]
  exact (succ_eq_succ_iff.mpr pw)
Proof state after:
no goals
Theorem: MyNat.succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : b = a + w
⊢ succ a ≤ succ b
Tactic:
exists w
Proof state after:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ a + w
Theorem: MyNat.succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ a + w
Tactic:
rw [succ_add]
Proof state after:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ (a + w)
Theorem: MyNat.succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ (a + w)
Tactic:
exact (succ_eq_succ_iff.mpr pw)
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
a b : Nat
⊢ a ≤ b ∨ b ≤ a
Tactic:
induction a with
| zero => apply Or.inl; exact (zero_le _)
| succ a' ih =>
  cases ih with
  | inl h =>
    cases h with
    | intro w pw =>
      cases w with
      | zero =>
        apply Or.inr
        exists one
        rw [add_zero] at pw
        rw [← succ_eq_add_one]
        exact succ_eq_succ_iff.mpr (Eq.symm pw)
      | succ w' =>
        apply Or.inl
        exists w'
        rw [add_succ] at pw
        rw [pw, succ_add]
  | inr h =>
    apply Or.inr
    apply le_succ
    assumption
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case zero
b : Nat
⊢ zero ≤ b ∨ b ≤ zero
Tactic:
apply Or.inl
Proof state after:
case zero.h
b : Nat
⊢ zero ≤ b
Theorem: MyNat.le_total
Proof state before:
case zero.h
b : Nat
⊢ zero ≤ b
Tactic:
exact (zero_le _)
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ
b a' : Nat
ih : a' ≤ b ∨ b ≤ a'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases ih with
| inl h =>
  cases h with
  | intro w pw =>
    cases w with
    | zero =>
      apply Or.inr
      exists one
      rw [add_zero] at pw
      rw [← succ_eq_add_one]
      exact succ_eq_succ_iff.mpr (Eq.symm pw)
    | succ w' =>
      apply Or.inl
      exists w'
      rw [add_succ] at pw
      rw [pw, succ_add]
| inr h =>
  apply Or.inr
  apply le_succ
  assumption
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ.inl
b a' : Nat
h : a' ≤ b
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases h with
| intro w pw =>
  cases w with
  | zero =>
    apply Or.inr
    exists one
    rw [add_zero] at pw
    rw [← succ_eq_add_one]
    exact succ_eq_succ_iff.mpr (Eq.symm pw)
  | succ w' =>
    apply Or.inl
    exists w'
    rw [add_succ] at pw
    rw [pw, succ_add]
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro
b a' w : Nat
pw : b = a' + w
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases w with
| zero =>
  apply Or.inr
  exists one
  rw [add_zero] at pw
  rw [← succ_eq_add_one]
  exact succ_eq_succ_iff.mpr (Eq.symm pw)
| succ w' =>
  apply Or.inl
  exists w'
  rw [add_succ] at pw
  rw [pw, succ_add]
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.zero
b a' : Nat
pw : b = a' + zero
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inr
Proof state after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ b ≤ succ a'
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ b ≤ succ a'
Tactic:
exists one
Proof state after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ succ a' = b + one
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ succ a' = b + one
Tactic:
rw [add_zero] at pw
Proof state after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = b + one
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = b + one
Tactic:
rw [← succ_eq_add_one]
Proof state after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = succ b
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = succ b
Tactic:
exact succ_eq_succ_iff.mpr (Eq.symm pw)
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.succ
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inl
Proof state after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b
Tactic:
exists w'
Proof state after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ b = succ a' + w'
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ b = succ a' + w'
Tactic:
rw [add_succ] at pw
Proof state after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = succ (a' + w')
⊢ b = succ a' + w'
Theorem: MyNat.le_total
Proof state before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = succ (a' + w')
⊢ b = succ a' + w'
Tactic:
rw [pw, succ_add]
Proof state after:
no goals
Theorem: MyNat.le_total
Proof state before:
case succ.inr
b a' : Nat
h : b ≤ a'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inr
Proof state after:
case succ.inr.h
b a' : Nat
h : b ≤ a'
⊢ b ≤ succ a'
Theorem: MyNat.le_total
Proof state before:
case succ.inr.h
b a' : Nat
h : b ≤ a'
⊢ b ≤ succ a'
Tactic:
apply le_succ
Proof state after:
case succ.inr.h.a
b a' : Nat
h : b ≤ a'
⊢ b ≤ a'
Theorem: MyNat.le_total
Proof state before:
case succ.inr.h.a
b a' : Nat
h : b ≤ a'
⊢ b ≤ a'
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.le_succ_self
Proof state before:
a : Nat
⊢ a ≤ succ a
Tactic:
exists one
Proof state after:
no goals
Theorem: MyNat.add_le_add_right
Proof state before:
a b : Nat
⊢ a ≤ b → ∀ (t : Nat), a + t ≤ b + t
Tactic:
intro h t
Proof state after:
a b : Nat
h : a ≤ b
t : Nat
⊢ a + t ≤ b + t
Theorem: MyNat.add_le_add_right
Proof state before:
a b : Nat
h : a ≤ b
t : Nat
⊢ a + t ≤ b + t
Tactic:
cases h with
| intro w pw =>
  exists w
  rw [pw]
  simp
Proof state after:
no goals
Theorem: MyNat.add_le_add_right
Proof state before:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + t ≤ b + t
Tactic:
exists w
Proof state after:
case intro
a b t w : Nat
pw : b = a + w
⊢ b + t = a + t + w
Theorem: MyNat.add_le_add_right
Proof state before:
case intro
a b t w : Nat
pw : b = a + w
⊢ b + t = a + t + w
Tactic:
rw [pw]
Proof state after:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + w + t = a + t + w
Theorem: MyNat.add_le_add_right
Proof state before:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + w + t = a + t + w
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.le_of_succ_le_succ
Proof state before:
a b : Nat
⊢ succ a ≤ succ b → a ≤ b
Tactic:
intro h
Proof state after:
a b : Nat
h : succ a ≤ succ b
⊢ a ≤ b
Theorem: MyNat.le_of_succ_le_succ
Proof state before:
a b : Nat
h : succ a ≤ succ b
⊢ a ≤ b
Tactic:
cases h with
| intro w pw =>
  exists w
  rw [succ_add] at pw
  exact (succ_inj pw)
Proof state after:
no goals
Theorem: MyNat.le_of_succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : succ b = succ a + w
⊢ a ≤ b
Tactic:
exists w
Proof state after:
case intro
a b w : Nat
pw : succ b = succ a + w
⊢ b = a + w
Theorem: MyNat.le_of_succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : succ b = succ a + w
⊢ b = a + w
Tactic:
rw [succ_add] at pw
Proof state after:
case intro
a b w : Nat
pw : succ b = succ (a + w)
⊢ b = a + w
Theorem: MyNat.le_of_succ_le_succ
Proof state before:
case intro
a b w : Nat
pw : succ b = succ (a + w)
⊢ b = a + w
Tactic:
exact (succ_inj pw)
Proof state after:
no goals
Theorem: MyNat.not_succ_le_self
Proof state before:
a : Nat
⊢ ¬succ a ≤ a
Tactic:
intro h
Proof state after:
a : Nat
h : succ a ≤ a
⊢ False
Theorem: MyNat.not_succ_le_self
Proof state before:
a : Nat
h : succ a ≤ a
⊢ False
Tactic:
cases h with
| intro w pw =>
  rw [succ_eq_add_one, add_comm_right, add_assoc] at pw
  have hw : w + one = zero := eq_zero_of_add_right_eq_self (Eq.symm pw)
  have _ : one = zero := add_left_eq_zero hw
  contradiction
Proof state after:
no goals
Theorem: MyNat.not_succ_le_self
Proof state before:
case intro
a w : Nat
pw : a = succ a + w
⊢ False
Tactic:
rw [succ_eq_add_one, add_comm_right, add_assoc] at pw
Proof state after:
case intro
a w : Nat
pw : a = a + (w + one)
⊢ False
Theorem: MyNat.not_succ_le_self
Proof state before:
case intro
a w : Nat
pw : a = a + (w + one)
⊢ False
Tactic:
have hw : w + one = zero := eq_zero_of_add_right_eq_self (Eq.symm pw)
Proof state after:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
⊢ False
Theorem: MyNat.not_succ_le_self
Proof state before:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
⊢ False
Tactic:
have _ : one = zero := add_left_eq_zero hw
Proof state after:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
x✝ : one = zero
⊢ False
Theorem: MyNat.not_succ_le_self
Proof state before:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
x✝ : one = zero
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.add_le_add_left
Proof state before:
a b : Nat
h : a ≤ b
t : Nat
⊢ t + a ≤ t + b
Tactic:
have _ : a + t ≤ b + t := add_le_add_right h t
Proof state after:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ t + a ≤ t + b
Theorem: MyNat.add_le_add_left
Proof state before:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ t + a ≤ t + b
Tactic:
rw [add_comm t a, add_comm t b]
Proof state after:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ a + t ≤ b + t
Theorem: MyNat.add_le_add_left
Proof state before:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ a + t ≤ b + t
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.lt_aux_one
Proof state before:
a b : Nat
⊢ a ≤ b ∧ ¬b ≤ a → succ a ≤ b
Tactic:
intro h
Proof state after:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
⊢ succ a ≤ b
Theorem: MyNat.lt_aux_one
Proof state before:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
⊢ succ a ≤ b
Tactic:
let ⟨⟨w, pw⟩, hc⟩ := h
Proof state after:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
w : Nat
pw : b = a + w
hc : ¬b ≤ a
⊢ succ a ≤ b
Theorem: MyNat.lt_aux_one
Proof state before:
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
w : Nat
pw : b = a + w
hc : ¬b ≤ a
⊢ succ a ≤ b
Tactic:
cases w with
| zero =>
  rw [add_zero] at pw
  have _ : b ≤ a := pw ▸ (le_refl b)  contradiction
| succ w' =>
  exists w'
  rw [pw, add_succ, succ_add]
Proof state after:
no goals
Theorem: MyNat.lt_aux_one
Proof state before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a + zero
⊢ succ a ≤ b
Tactic:
rw [add_zero] at pw
Proof state after:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
⊢ succ a ≤ b
Theorem: MyNat.lt_aux_one
Proof state before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
⊢ succ a ≤ b
Tactic:
have _ : b ≤ a := pw ▸ (le_refl b)
Proof state after:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
x✝ : b ≤ a
⊢ succ a ≤ b
Theorem: MyNat.lt_aux_one
Proof state before:
case zero
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
pw : b = a
x✝ : b ≤ a
⊢ succ a ≤ b
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.lt_aux_one
Proof state before:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ succ a ≤ b
Tactic:
exists w'
Proof state after:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ b = succ a + w'
Theorem: MyNat.lt_aux_one
Proof state before:
case succ
a b : Nat
h : a ≤ b ∧ ¬b ≤ a
hc : ¬b ≤ a
w' : Nat
pw : b = a + succ w'
⊢ b = succ a + w'
Tactic:
rw [pw, add_succ, succ_add]
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
⊢ succ a ≤ b → a ≤ b ∧ ¬b ≤ a
Tactic:
intro
| ⟨w , pw⟩  =>
  constructor
  case left =>
    exists (w + one)
    rw [pw, succ_eq_add_one]
    simp
  case right =>
    intro
    have _ : succ a ≤ b := by exists w
    have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
    apply (@not_succ_le_self a)
    assumption
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b ∧ ¬b ≤ a
Tactic:
constructor
Proof state after:
case left
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b

case right
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b
Tactic:
case left =>
  exists (w + one)
  rw [pw, succ_eq_add_one]
  simp
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
Tactic:
case right =>
  intro
  have _ : succ a ≤ b := by exists w
  have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
  apply (@not_succ_le_self a)
  assumption
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a ≤ b
Tactic:
exists (w + one)
Proof state after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ b = a + (w + one)
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ b = a + (w + one)
Tactic:
rw [pw, succ_eq_add_one]
Proof state after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a + one + w = a + (w + one)
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ a + one + w = a + (w + one)
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
⊢ ¬b ≤ a
Tactic:
intro
Proof state after:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ False
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ False
Tactic:
have _ : succ a ≤ b := by exists w
Proof state after:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ False
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ False
Tactic:
have _ : succ a ≤ a := by apply (@le_trans (succ a) b) <;> assumption
Proof state after:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ False
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ False
Tactic:
apply (@not_succ_le_self a)
Proof state after:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ succ a ≤ a
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝² : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝¹ : succ a ≤ b
x✝ : succ a ≤ a
⊢ succ a ≤ a
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
⊢ succ a ≤ b
Tactic:
exists w
Proof state after:
no goals
Theorem: MyNat.lt_aux_two
Proof state before:
a b : Nat
x✝¹ : succ a ≤ b
w : Nat
pw : b = succ a + w
a✝ : b ≤ a
x✝ : succ a ≤ b
⊢ succ a ≤ a
Tactic:
apply (@le_trans (succ a) b) <;> assumption
Proof state after:
no goals
Theorem: MyNat.lt_iff_succ_le
Proof state before:
a b : Nat
⊢ a < b ↔ succ a ≤ b
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ a < b → succ a ≤ b

case mpr
a b : Nat
⊢ succ a ≤ b → a < b
Theorem: MyNat.lt_iff_succ_le
Proof state before:
a b : Nat
⊢ a < b → succ a ≤ b
Tactic:
case mp => exact lt_aux_one _ _
Proof state after:
no goals
Theorem: MyNat.lt_iff_succ_le
Proof state before:
a b : Nat
⊢ succ a ≤ b → a < b
Tactic:
case mpr => exact lt_aux_two _ _
Proof state after:
no goals
Theorem: MyNat.lt_iff_succ_le
Proof state before:
a b : Nat
⊢ a < b → succ a ≤ b
Tactic:
exact lt_aux_one _ _
Proof state after:
no goals
Theorem: MyNat.lt_iff_succ_le
Proof state before:
a b : Nat
⊢ succ a ≤ b → a < b
Tactic:
exact lt_aux_two _ _
Proof state after:
no goals
Theorem: T2
Proof state before:
a b c d e : Nat
h1 : a = b
h2 : b = c + 1
h3 : c = d
h4 : e = 1 + d
⊢ c + 1 = d + 1
Tactic:
rw [h3]
Proof state after:
no goals
Theorem: T2
Proof state before:
a b c d e : Nat
h1 : a = b
h2 : b = c + 1
h3 : c = d
h4 : e = 1 + d
⊢ d + 1 = e
Tactic:
rw [Nat.add_comm, h4]
Proof state after:
no goals
Theorem: T3
Proof state before:
a b c d e : Nat
h1 : a = b
h2 : b = c + 1
h3 : c = d
h4 : e = 1 + d
⊢ a = e
Tactic:
simp [h1, h2, h3, h4, Nat.add_comm]
Proof state after:
no goals
Theorem: polynomial.minus_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Polynomial.lt p) (Polynomial.lt (p - Polynomial.Lt p)) == Ordering.lt) = true
Tactic:
simp [Polynomial.Lt, Polynomial.lt, not_empty]
Proof state after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Std.RBSet.min! p)
        (if Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false then
          Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))
        else (1, get_variables n)) ==
      Ordering.lt) =
    true
Theorem: polynomial.minus_lt
Proof state before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Std.RBSet.min! p)
        (if Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false then
          Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))
        else (1, get_variables n)) ==
      Ordering.lt) =
    true
Tactic:
split
Proof state after:
case inl
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))) == Ordering.lt) = true

case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true