internlm/Lean-Github huggingface dataset:
Theorem: Pos.lt_irrefl
Proof state before:
x : Pos
⊢ ¬x < x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ ¬x.toNat > x.toNat
Theorem: Pos.lt_irrefl
Proof state before:
x : Pos
⊢ ¬x.toNat > x.toNat
Tactic:
exact Nat.lt_irrefl _
Proof state after:
no goals
Theorem: Pos.lt_trans
Proof state before:
x y z : Pos
⊢ x < y → y < z → x < z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat > x.toNat → z.toNat > y.toNat → z.toNat > x.toNat
Theorem: Pos.lt_trans
Proof state before:
x y z : Pos
⊢ y.toNat > x.toNat → z.toNat > y.toNat → z.toNat > x.toNat
Tactic:
exact Nat.lt_trans
Proof state after:
no goals
Theorem: Pos.lt_of_le_of_lt
Proof state before:
x y z : Pos
⊢ x ≤ y → y < z → x < z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat ≥ x.toNat → z.toNat > y.toNat → z.toNat > x.toNat
Theorem: Pos.lt_of_le_of_lt
Proof state before:
x y z : Pos
⊢ y.toNat ≥ x.toNat → z.toNat > y.toNat → z.toNat > x.toNat
Tactic:
exact Nat.lt_of_le_of_lt
Proof state after:
no goals
Theorem: Pos.lt_of_lt_of_le
Proof state before:
x y z : Pos
⊢ x < y → y ≤ z → x < z
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat > x.toNat → z.toNat ≥ y.toNat → z.toNat > x.toNat
Theorem: Pos.lt_of_lt_of_le
Proof state before:
x y z : Pos
⊢ y.toNat > x.toNat → z.toNat ≥ y.toNat → z.toNat > x.toNat
Tactic:
exact Nat.lt_of_lt_of_le
Proof state after:
no goals
Theorem: Pos.le_of_eq
Proof state before:
x y : Pos
⊢ x = y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat = y.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_eq
Proof state before:
x y : Pos
⊢ x.toNat = y.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_eq
Proof state after:
no goals
Theorem: Pos.le_of_lt
Proof state before:
x y : Pos
⊢ x < y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_lt
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_lt
Proof state after:
no goals
Theorem: Pos.ne_of_lt
Proof state before:
x y : Pos
⊢ x < y → x ≠ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → x.toNat ≠ y.toNat
Theorem: Pos.ne_of_lt
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → x.toNat ≠ y.toNat
Tactic:
exact Nat.ne_of_lt
Proof state after:
no goals
Theorem: Pos.lt_of_le_of_ne
Proof state before:
x y : Pos
⊢ x ≤ y → x ≠ y → x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat ≠ y.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_le_of_ne
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat ≠ y.toNat → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_le_of_ne
Proof state after:
no goals
Theorem: Pos.le_of_not_gt
Proof state before:
x y : Pos
⊢ ¬x > y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ ¬x.toNat > y.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_not_gt
Proof state before:
x y : Pos
⊢ ¬x.toNat > y.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_not_gt
Proof state after:
no goals
Theorem: Pos.lt_of_not_ge
Proof state before:
x y : Pos
⊢ ¬x ≥ y → x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ ¬x.toNat ≥ y.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_not_ge
Proof state before:
x y : Pos
⊢ ¬x.toNat ≥ y.toNat → y.toNat > x.toNat
Tactic:
exact Nat.gt_of_not_le
Proof state after:
no goals
Theorem: Pos.not_le_of_gt
Proof state before:
x y : Pos
⊢ x > y → ¬x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat > y.toNat → ¬y.toNat ≥ x.toNat
Theorem: Pos.not_le_of_gt
Proof state before:
x y : Pos
⊢ x.toNat > y.toNat → ¬y.toNat ≥ x.toNat
Tactic:
exact Nat.not_le_of_gt
Proof state after:
no goals
Theorem: Pos.not_lt_of_ge
Proof state before:
x y : Pos
⊢ x ≥ y → ¬x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ x.toNat ≥ y.toNat → ¬y.toNat > x.toNat
Theorem: Pos.not_lt_of_ge
Proof state before:
x y : Pos
⊢ x.toNat ≥ y.toNat → ¬y.toNat > x.toNat
Tactic:
exact Nat.not_lt_of_ge
Proof state after:
no goals
Theorem: Pos.eq_or_lt_of_le
Proof state before:
x y : Pos
⊢ x ≤ y → x = y ∨ x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat = y.toNat ∨ y.toNat > x.toNat
Theorem: Pos.eq_or_lt_of_le
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → x.toNat = y.toNat ∨ y.toNat > x.toNat
Tactic:
exact Nat.eq_or_lt_of_le
Proof state after:
no goals
Theorem: Pos.lt_or_ge
Proof state before:
x y : Pos
⊢ x < y ∨ x ≥ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat ∨ x.toNat ≥ y.toNat
Theorem: Pos.lt_or_ge
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat ∨ x.toNat ≥ y.toNat
Tactic:
exact Nat.lt_or_ge ..
Proof state after:
no goals
Theorem: Pos.one_le
Proof state before:
x : Pos
⊢ 1 ≤ x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat ≥ 1
Theorem: Pos.one_le
Proof state before:
x : Pos
⊢ x.toNat ≥ 1
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case h
x : Pos
⊢ 0 < x.toNat
Theorem: Pos.one_le
Proof state before:
case h
x : Pos
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.not_lt_one
Proof state before:
x : Pos
⊢ ¬x < 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ ¬1 > x.toNat
Theorem: Pos.not_lt_one
Proof state before:
x : Pos
⊢ ¬1 > x.toNat
Tactic:
intro h
Proof state after:
x : Pos
h : 1 > x.toNat
⊢ False
Theorem: Pos.not_lt_one
Proof state before:
x : Pos
h : 1 > x.toNat
⊢ False
Tactic:
absurd h
Proof state after:
x : Pos
h : 1 > x.toNat
⊢ ¬1 > x.toNat
Theorem: Pos.not_lt_one
Proof state before:
x : Pos
h : 1 > x.toNat
⊢ ¬1 > x.toNat
Tactic:
apply Nat.not_lt_of_ge
Proof state after:
case a
x : Pos
h : 1 > x.toNat
⊢ x.toNat ≥ 1
Theorem: Pos.not_lt_one
Proof state before:
case a
x : Pos
h : 1 > x.toNat
⊢ x.toNat ≥ 1
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case a.h
x : Pos
h : 1 > x.toNat
⊢ 0 < x.toNat
Theorem: Pos.not_lt_one
Proof state before:
case a.h
x : Pos
h : 1 > x.toNat
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.one_lt_succ
Proof state before:
x : Pos
⊢ 1 < x + 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat + 1 > 1
Theorem: Pos.one_lt_succ
Proof state before:
x : Pos
⊢ x.toNat + 1 > 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a
x : Pos
⊢ 0 < x.toNat
Theorem: Pos.one_lt_succ
Proof state before:
case a
x : Pos
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.not_succ_le_one
Proof state before:
x : Pos
⊢ ¬x + 1 ≤ 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ ¬1 ≥ x.toNat + 1
Theorem: Pos.not_succ_le_one
Proof state before:
x : Pos
⊢ ¬1 ≥ x.toNat + 1
Tactic:
intro h
Proof state after:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ False
Theorem: Pos.not_succ_le_one
Proof state before:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ False
Tactic:
absurd h
Proof state after:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ ¬1 ≥ x.toNat + 1
Theorem: Pos.not_succ_le_one
Proof state before:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ ¬1 ≥ x.toNat + 1
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
x : Pos
h : 1 ≥ x.toNat + 1
⊢ x.toNat + 1 > 1
Theorem: Pos.not_succ_le_one
Proof state before:
case h
x : Pos
h : 1 ≥ x.toNat + 1
⊢ x.toNat + 1 > 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case h.a
x : Pos
h : 1 ≥ x.toNat + 1
⊢ 0 < x.toNat
Theorem: Pos.not_succ_le_one
Proof state before:
case h.a
x : Pos
h : 1 ≥ x.toNat + 1
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.le_succ_self
Proof state before:
x : Pos
⊢ x ≤ x + 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat + 1 ≥ x.toNat
Theorem: Pos.le_succ_self
Proof state before:
x : Pos
⊢ x.toNat + 1 ≥ x.toNat
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Pos.lt_succ_self
Proof state before:
x : Pos
⊢ x < x + 1
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ x.toNat + 1 > x.toNat
Theorem: Pos.lt_succ_self
Proof state before:
x : Pos
⊢ x.toNat + 1 > x.toNat
Tactic:
exact Nat.lt_succ_self ..
Proof state after:
no goals
Theorem: Pos.not_succ_le_self
Proof state before:
x : Pos
⊢ ¬x + 1 ≤ x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ ¬x.toNat ≥ x.toNat + 1
Theorem: Pos.not_succ_le_self
Proof state before:
x : Pos
⊢ ¬x.toNat ≥ x.toNat + 1
Tactic:
exact Nat.not_succ_le_self _
Proof state after:
no goals
Theorem: Pos.not_succ_lt_self
Proof state before:
x : Pos
⊢ ¬x + 1 < x
Tactic:
by_toNat
Proof state after:
x : Pos
⊢ ¬x.toNat > x.toNat + 1
Theorem: Pos.not_succ_lt_self
Proof state before:
x : Pos
⊢ ¬x.toNat > x.toNat + 1
Tactic:
apply Nat.not_lt_of_ge
Proof state after:
case a
x : Pos
⊢ x.toNat + 1 ≥ x.toNat
Theorem: Pos.not_succ_lt_self
Proof state before:
case a
x : Pos
⊢ x.toNat + 1 ≥ x.toNat
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Pos.le_of_lt_succ
Proof state before:
x y : Pos
⊢ x < y + 1 → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat + 1 > x.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_lt_succ
Proof state before:
x y : Pos
⊢ y.toNat + 1 > x.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_lt_succ
Proof state after:
no goals
Theorem: Pos.lt_succ_of_le
Proof state before:
x y : Pos
⊢ x ≤ y → x < y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 > x.toNat
Theorem: Pos.lt_succ_of_le
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 > x.toNat
Tactic:
exact Nat.lt_succ_of_le
Proof state after:
no goals
Theorem: Pos.lt_of_succ_le
Proof state before:
x y : Pos
⊢ x + 1 ≤ y → x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat + 1 → y.toNat > x.toNat
Theorem: Pos.lt_of_succ_le
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat + 1 → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_succ_le
Proof state after:
no goals
Theorem: Pos.succ_le_of_lt
Proof state before:
x y : Pos
⊢ x < y → x + 1 ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat ≥ x.toNat + 1
Theorem: Pos.succ_le_of_lt
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat ≥ x.toNat + 1
Tactic:
exact Nat.succ_le_of_lt
Proof state after:
no goals
Theorem: Pos.le_succ_of_le
Proof state before:
x y : Pos
⊢ x ≤ y → x ≤ y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 ≥ x.toNat
Theorem: Pos.le_succ_of_le
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 ≥ x.toNat
Tactic:
exact Nat.le_succ_of_le
Proof state after:
no goals
Theorem: Pos.le_of_succ_le
Proof state before:
x y : Pos
⊢ x + 1 ≤ y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat + 1 → y.toNat ≥ x.toNat
Theorem: Pos.le_of_succ_le
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat + 1 → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_succ_le
Proof state after:
no goals
Theorem: Pos.succ_le_succ
Proof state before:
x y : Pos
⊢ x ≤ y → x + 1 ≤ y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 ≥ x.toNat + 1
Theorem: Pos.succ_le_succ
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → y.toNat + 1 ≥ x.toNat + 1
Tactic:
exact Nat.succ_le_succ
Proof state after:
no goals
Theorem: Pos.le_of_succ_le_succ
Proof state before:
x y : Pos
⊢ x + 1 ≤ y + 1 → x ≤ y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat + 1 ≥ x.toNat + 1 → y.toNat ≥ x.toNat
Theorem: Pos.le_of_succ_le_succ
Proof state before:
x y : Pos
⊢ y.toNat + 1 ≥ x.toNat + 1 → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_succ_le_succ
Proof state after:
no goals
Theorem: Pos.succ_lt_succ
Proof state before:
x y : Pos
⊢ x < y → x + 1 < y + 1
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat + 1 > x.toNat + 1
Theorem: Pos.succ_lt_succ
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → y.toNat + 1 > x.toNat + 1
Tactic:
exact Nat.succ_lt_succ
Proof state after:
no goals
Theorem: Pos.lt_of_succ_lt_succ
Proof state before:
x y : Pos
⊢ x + 1 < y + 1 → x < y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat + 1 > x.toNat + 1 → y.toNat > x.toNat
Theorem: Pos.lt_of_succ_lt_succ
Proof state before:
x y : Pos
⊢ y.toNat + 1 > x.toNat + 1 → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_succ_lt_succ
Proof state after:
no goals
Theorem: Pos.lt_add_right
Proof state before:
x y : Pos
⊢ x < x + y
Tactic:
induction y with
| one => exact Pos.lt_succ_self x
| succ y H => apply Pos.lt_trans H; rw [Pos.add_succ]; exact Pos.lt_succ_self (x + y)
Proof state after:
no goals
Theorem: Pos.lt_add_right
Proof state before:
case one
x : Pos
⊢ x < x + 1
Tactic:
exact Pos.lt_succ_self x
Proof state after:
no goals
Theorem: Pos.lt_add_right
Proof state before:
case succ
x y : Pos
H : x < x + y
⊢ x < x + (y + 1)
Tactic:
apply Pos.lt_trans H
Proof state after:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + (y + 1)
Theorem: Pos.lt_add_right
Proof state before:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + (y + 1)
Tactic:
rw [Pos.add_succ]
Proof state after:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + y + 1
Theorem: Pos.lt_add_right
Proof state before:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + y + 1
Tactic:
exact Pos.lt_succ_self (x + y)
Proof state after:
no goals
Theorem: Pos.lt_add_left
Proof state before:
x y : Pos
⊢ x < y + x
Tactic:
induction y with
| one => rw [Pos.one_add_eq_add_one]; exact Pos.lt_succ_self x
| succ y H => apply Pos.lt_trans H; rw [Pos.succ_add]; exact Pos.lt_succ_self (y + x)
Proof state after:
no goals
Theorem: Pos.lt_add_left
Proof state before:
case one
x : Pos
⊢ x < 1 + x
Tactic:
rw [Pos.one_add_eq_add_one]
Proof state after:
case one
x : Pos
⊢ x < x + 1
Theorem: Pos.lt_add_left
Proof state before:
case one
x : Pos
⊢ x < x + 1
Tactic:
exact Pos.lt_succ_self x
Proof state after:
no goals
Theorem: Pos.lt_add_left
Proof state before:
case succ
x y : Pos
H : x < y + x
⊢ x < y + 1 + x
Tactic:
apply Pos.lt_trans H
Proof state after:
case succ
x y : Pos
H : x < y + x
⊢ y + x < y + 1 + x
Theorem: Pos.lt_add_left
Proof state before:
case succ
x y : Pos
H : x < y + x
⊢ y + x < y + 1 + x
Tactic:
rw [Pos.succ_add]
Proof state after:
case succ
x y : Pos
H : x < y + x
⊢ y + x < y + x + 1
Theorem: Pos.lt_add_left
Proof state before:
case succ
x y : Pos
H : x < y + x
⊢ y + x < y + x + 1
Tactic:
exact Pos.lt_succ_self (y + x)
Proof state after:
no goals
Theorem: Pos.add_le_add_left
Proof state before:
x y : Pos
⊢ x ≤ y → ∀ (z : Pos), z + x ≤ z + y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), z.toNat + y.toNat ≥ z.toNat + x.toNat
Theorem: Pos.add_le_add_left
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), z.toNat + y.toNat ≥ z.toNat + x.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ z.toNat + y.toNat ≥ z.toNat + x.toNat
Theorem: Pos.add_le_add_left
Proof state before:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ z.toNat + y.toNat ≥ z.toNat + x.toNat
Tactic:
apply Nat.add_le_add_left h
Proof state after:
no goals
Theorem: Pos.add_le_add_right
Proof state before:
x y : Pos
⊢ x ≤ y → ∀ (z : Pos), x + z ≤ y + z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), y.toNat + z.toNat ≥ x.toNat + z.toNat
Theorem: Pos.add_le_add_right
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), y.toNat + z.toNat ≥ x.toNat + z.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ y.toNat + z.toNat ≥ x.toNat + z.toNat
Theorem: Pos.add_le_add_right
Proof state before:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ y.toNat + z.toNat ≥ x.toNat + z.toNat
Tactic:
apply Nat.add_le_add_right h
Proof state after:
no goals
Theorem: Pos.le_of_add_le_add_left
Proof state before:
x y z : Pos
⊢ z + x ≤ z + y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ z.toNat + y.toNat ≥ z.toNat + x.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_add_le_add_left
Proof state before:
x y z : Pos
⊢ z.toNat + y.toNat ≥ z.toNat + x.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_add_le_add_left
Proof state after:
no goals
Theorem: Pos.le_of_add_le_add_right
Proof state before:
x y z : Pos
⊢ x + z ≤ y + z → x ≤ y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat + z.toNat ≥ x.toNat + z.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_add_le_add_right
Proof state before:
x y z : Pos
⊢ y.toNat + z.toNat ≥ x.toNat + z.toNat → y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_add_le_add_right
Proof state after:
no goals
Theorem: Pos.add_le_add
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ ≤ y₁ → x₂ ≤ y₂ → x₁ + x₂ ≤ y₁ + y₂
Tactic:
by_toNat
Proof state after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat + y₂.toNat ≥ x₁.toNat + x₂.toNat
Theorem: Pos.add_le_add
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat + y₂.toNat ≥ x₁.toNat + x₂.toNat
Tactic:
exact Nat.add_le_add
Proof state after:
no goals
Theorem: Pos.add_lt_add_left
Proof state before:
x y : Pos
⊢ x < y → ∀ (z : Pos), z + x < z + y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), z.toNat + y.toNat > z.toNat + x.toNat
Theorem: Pos.add_lt_add_left
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), z.toNat + y.toNat > z.toNat + x.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat + y.toNat > z.toNat + x.toNat
Theorem: Pos.add_lt_add_left
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat + y.toNat > z.toNat + x.toNat
Tactic:
apply Nat.add_lt_add_left h
Proof state after:
no goals
Theorem: Pos.add_lt_add_right
Proof state before:
x y : Pos
⊢ x < y → ∀ (z : Pos), x + z < y + z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), y.toNat + z.toNat > x.toNat + z.toNat
Theorem: Pos.add_lt_add_right
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), y.toNat + z.toNat > x.toNat + z.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ y.toNat + z.toNat > x.toNat + z.toNat
Theorem: Pos.add_lt_add_right
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ y.toNat + z.toNat > x.toNat + z.toNat
Tactic:
apply Nat.add_lt_add_right h
Proof state after:
no goals
Theorem: Pos.lt_of_add_lt_add_left
Proof state before:
x y z : Pos
⊢ z + x < z + y → x < y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ z.toNat + y.toNat > z.toNat + x.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_add_lt_add_left
Proof state before:
x y z : Pos
⊢ z.toNat + y.toNat > z.toNat + x.toNat → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_add_lt_add_left
Proof state after:
no goals
Theorem: Pos.lt_of_add_lt_add_right
Proof state before:
x y z : Pos
⊢ x + z < y + z → x < y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat + z.toNat > x.toNat + z.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_add_lt_add_right
Proof state before:
x y z : Pos
⊢ y.toNat + z.toNat > x.toNat + z.toNat → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_add_lt_add_right
Proof state after:
no goals
Theorem: Pos.add_lt_add
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ < y₁ → x₂ < y₂ → x₁ + x₂ < y₁ + y₂
Tactic:
by_toNat
Proof state after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat + y₂.toNat > x₁.toNat + x₂.toNat
Theorem: Pos.add_lt_add
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat + y₂.toNat > x₁.toNat + x₂.toNat
Tactic:
exact Nat.add_lt_add
Proof state after:
no goals
Theorem: Pos.mul_le_mul_left
Proof state before:
x y : Pos
⊢ x ≤ y → ∀ (z : Pos), z * x ≤ z * y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), z.toNat * y.toNat ≥ z.toNat * x.toNat
Theorem: Pos.mul_le_mul_left
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), z.toNat * y.toNat ≥ z.toNat * x.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ z.toNat * y.toNat ≥ z.toNat * x.toNat
Theorem: Pos.mul_le_mul_left
Proof state before:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ z.toNat * y.toNat ≥ z.toNat * x.toNat
Tactic:
apply Nat.mul_le_mul_left _ h
Proof state after:
no goals
Theorem: Pos.mul_le_mul_right
Proof state before:
x y : Pos
⊢ x ≤ y → ∀ (z : Pos), x * z ≤ y * z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), y.toNat * z.toNat ≥ x.toNat * z.toNat
Theorem: Pos.mul_le_mul_right
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Pos), y.toNat * z.toNat ≥ x.toNat * z.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ y.toNat * z.toNat ≥ x.toNat * z.toNat
Theorem: Pos.mul_le_mul_right
Proof state before:
x y : Pos
h : y.toNat ≥ x.toNat
z : Pos
⊢ y.toNat * z.toNat ≥ x.toNat * z.toNat
Tactic:
apply Nat.mul_le_mul_right _ h
Proof state after:
no goals
Theorem: Pos.le_of_mul_le_mul_left
Proof state before:
x y z : Pos
⊢ z * x ≤ z * y → x ≤ y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ z.toNat * y.toNat ≥ z.toNat * x.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_mul_le_mul_left
Proof state before:
x y z : Pos
⊢ z.toNat * y.toNat ≥ z.toNat * x.toNat → y.toNat ≥ x.toNat
Tactic:
intro h
Proof state after:
x y z : Pos
h : z.toNat * y.toNat ≥ z.toNat * x.toNat
⊢ y.toNat ≥ x.toNat
Theorem: Pos.le_of_mul_le_mul_left
Proof state before:
x y z : Pos
h : z.toNat * y.toNat ≥ z.toNat * x.toNat
⊢ y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_mul_le_mul_of_pos_left (Nat.zero_lt _) h
Proof state after:
no goals
Theorem: Pos.le_of_mul_le_mul_right
Proof state before:
x y z : Pos
⊢ x * z ≤ y * z → x ≤ y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat * z.toNat ≥ x.toNat * z.toNat → y.toNat ≥ x.toNat
Theorem: Pos.le_of_mul_le_mul_right
Proof state before:
x y z : Pos
⊢ y.toNat * z.toNat ≥ x.toNat * z.toNat → y.toNat ≥ x.toNat
Tactic:
intro h
Proof state after:
x y z : Pos
h : y.toNat * z.toNat ≥ x.toNat * z.toNat
⊢ y.toNat ≥ x.toNat
Theorem: Pos.le_of_mul_le_mul_right
Proof state before:
x y z : Pos
h : y.toNat * z.toNat ≥ x.toNat * z.toNat
⊢ y.toNat ≥ x.toNat
Tactic:
exact Nat.le_of_mul_le_mul_of_pos_right (Nat.zero_lt _) h
Proof state after:
no goals
Theorem: Pos.mul_le_mul
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ ≤ y₁ → x₂ ≤ y₂ → x₁ * x₂ ≤ y₁ * y₂
Tactic:
by_toNat
Proof state after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat * y₂.toNat ≥ x₁.toNat * x₂.toNat
Theorem: Pos.mul_le_mul
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat * y₂.toNat ≥ x₁.toNat * x₂.toNat
Tactic:
exact Nat.mul_le_mul
Proof state after:
no goals
Theorem: Pos.mul_lt_mul_left
Proof state before:
x y : Pos
⊢ x < y → ∀ (z : Pos), z * x < z * y
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), z.toNat * y.toNat > z.toNat * x.toNat
Theorem: Pos.mul_lt_mul_left
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), z.toNat * y.toNat > z.toNat * x.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat * y.toNat > z.toNat * x.toNat
Theorem: Pos.mul_lt_mul_left
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat * y.toNat > z.toNat * x.toNat
Tactic:
apply Nat.mul_lt_mul_of_pos_left h
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat > 0
Theorem: Pos.mul_lt_mul_left
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat > 0
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.mul_lt_mul_right
Proof state before:
x y : Pos
⊢ x < y → ∀ (z : Pos), x * z < y * z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), y.toNat * z.toNat > x.toNat * z.toNat
Theorem: Pos.mul_lt_mul_right
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ (z : Pos), y.toNat * z.toNat > x.toNat * z.toNat
Tactic:
intro h z
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ y.toNat * z.toNat > x.toNat * z.toNat
Theorem: Pos.mul_lt_mul_right
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ y.toNat * z.toNat > x.toNat * z.toNat
Tactic:
apply Nat.mul_lt_mul_of_pos_right h
Proof state after:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat > 0
Theorem: Pos.mul_lt_mul_right
Proof state before:
x y : Pos
h : y.toNat > x.toNat
z : Pos
⊢ z.toNat > 0
Tactic:
exact Nat.zero_lt _
Proof state after:
no goals
Theorem: Pos.lt_of_mul_lt_mul_left
Proof state before:
x y z : Pos
⊢ z * x < z * y → x < y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ z.toNat * y.toNat > z.toNat * x.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_mul_lt_mul_left
Proof state before:
x y z : Pos
⊢ z.toNat * y.toNat > z.toNat * x.toNat → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_mul_lt_mul_left
Proof state after:
no goals