internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝¹ : n < m
this✝ : k < j
this : n + k < m + j
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
have : compare (n + k) (m + j) = Ordering.lt := compare_lt.mpr this
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝² : n < m
this✝¹ : k < j
this✝ : n + k < m + j
this : compare (n + k) (m + j) = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝² : n < m
this✝¹ : k < j
this✝ : n + k < m + j
this : compare (n + k) (m + j) = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
⊢ compare n m = Ordering.eq → compare k j = Ordering.eq → compare (n + k) (m + j) = Ordering.eq
Tactic:
intro (_ : compare n m = Ordering.eq) (_ : compare k j = Ordering.eq)
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : n ≃ m := compare_eq.mp ‹compare n m = Ordering.eq›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this : n ≃ m
⊢ compare (n + k) (m + j) = Ordering.eq
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this : n ≃ m
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : k ≃ j := compare_eq.mp ‹compare k j = Ordering.eq›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝ : n ≃ m
this : k ≃ j
⊢ compare (n + k) (m + j) = Ordering.eq
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝ : n ≃ m
this : k ≃ j
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : n + k ≃ m + j := calc
  n + k ≃ m + k := AA.substL ‹n ≃ m›
  m + k ≃ m + j := AA.substR ‹k ≃ j›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝¹ : n ≃ m
this✝ : k ≃ j
this : n + k ≃ m + j
⊢ compare (n + k) (m + j) = Ordering.eq
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝¹ : n ≃ m
this✝ : k ≃ j
this : n + k ≃ m + j
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
have : compare (n + k) (m + j) = Ordering.eq := compare_eq.mpr this
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝² : n ≃ m
this✝¹ : k ≃ j
this✝ : n + k ≃ m + j
this : compare (n + k) (m + j) = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.eq
x✝ : compare k j = Ordering.eq
this✝² : n ≃ m
this✝¹ : k ≃ j
this✝ : n + k ≃ m + j
this : compare (n + k) (m + j) = Ordering.eq
⊢ compare (n + k) (m + j) = Ordering.eq
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
⊢ compare n m = Ordering.gt → compare k j = Ordering.gt → compare (n + k) (m + j) = Ordering.gt
Tactic:
intro (_ : compare n m = Ordering.gt) (_ : compare k j = Ordering.gt)
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : n > m := compare_gt.mp ‹compare n m = Ordering.gt›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this : n > m
⊢ compare (n + k) (m + j) = Ordering.gt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this : n > m
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : k > j := compare_gt.mp ‹compare k j = Ordering.gt›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝ : n > m
this : k > j
⊢ compare (n + k) (m + j) = Ordering.gt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝ : n > m
this : k > j
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : m + j < n + k := calc
  m + j < m + k := lt_substR_add ‹j < k›
  m + k < n + k := lt_substL_add ‹m < n›
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝¹ : n > m
this✝ : k > j
this : m + j < n + k
⊢ compare (n + k) (m + j) = Ordering.gt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝¹ : n > m
this✝ : k > j
this : m + j < n + k
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
have : compare (n + k) (m + j) = Ordering.gt := compare_gt.mpr this
Proof state after:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝² : n > m
this✝¹ : k > j
this✝ : m + j < n + k
this : compare (n + k) (m + j) = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Theorem: Lean4Axiomatic.Natural.add_preserves_compare
Proof state before:
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.gt
x✝ : compare k j = Ordering.gt
this✝² : n > m
this✝¹ : k > j
this✝ : m + j < n + k
this : compare (n + k) (m + j) = Ordering.gt
⊢ compare (n + k) (m + j) = Ordering.gt
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ q ↔ sgn (p - q) ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ q → sgn (p - q) ≃ 0

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ sgn (p - q) ≃ 0 → p ≃ q
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ q → sgn (p - q) ≃ 0
Tactic:
case mp =>
  intro (_ : p ≃ q)
  show sgn (p - q) ≃ 0
  have : p - q ≃ 0 := sub_eqv_zero_iff_eqv.mpr ‹p ≃ q›
  have : sgn (p - q) ≃ 0 := sgn_zero.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ sgn (p - q) ≃ 0 → p ≃ q
Tactic:
case mpr =>
  intro (_ : sgn (p - q) ≃ 0)
  show p ≃ q
  have : p - q ≃ 0 := sgn_zero.mpr ‹sgn (p - q) ≃ 0›
  have : p ≃ q := sub_eqv_zero_iff_eqv.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ q → sgn (p - q) ≃ 0
Tactic:
intro (_ : p ≃ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
⊢ sgn (p - q) ≃ 0
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
⊢ sgn (p - q) ≃ 0
Tactic:
have : p - q ≃ 0 := sub_eqv_zero_iff_eqv.mpr ‹p ≃ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
this : p - q ≃ 0
⊢ sgn (p - q) ≃ 0
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
this : p - q ≃ 0
⊢ sgn (p - q) ≃ 0
Tactic:
have : sgn (p - q) ≃ 0 := sgn_zero.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
this✝ : p - q ≃ 0
this : sgn (p - q) ≃ 0
⊢ sgn (p - q) ≃ 0
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≃ q
this✝ : p - q ≃ 0
this : sgn (p - q) ≃ 0
⊢ sgn (p - q) ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ sgn (p - q) ≃ 0 → p ≃ q
Tactic:
intro (_ : sgn (p - q) ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
⊢ p ≃ q
Tactic:
have : p - q ≃ 0 := sgn_zero.mpr ‹sgn (p - q) ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
this : p - q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
this : p - q ≃ 0
⊢ p ≃ q
Tactic:
have : p ≃ q := sub_eqv_zero_iff_eqv.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
this✝ : p - q ≃ 0
this : p ≃ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.eqv_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : sgn (p - q) ≃ 0
this✝ : p - q ≃ 0
this : p ≃ q
⊢ p ≃ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ p < 0 ↔ sgn p ≃ -1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ p < 0 → sgn p ≃ -1

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ sgn p ≃ -1 → p < 0
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ p < 0 → sgn p ≃ -1
Tactic:
case mp =>
  intro (_ : p < 0)
  show sgn p ≃ -1
  calc
    _ ≃ sgn p       := Rel.refl
    _ ≃ sgn (p - 0) := sgn_subst (eqv_symm sub_zero)
    _ ≃ -1          := lt_sgn.mp ‹p < 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ sgn p ≃ -1 → p < 0
Tactic:
case mpr =>
  intro (_ : sgn p ≃ -1)
  show p < 0
  have : sgn (p - 0) ≃ -1 := calc
    _ ≃ sgn (p - 0) := Rel.refl
    _ ≃ sgn p       := sgn_subst sub_zero
    _ ≃ -1          := ‹sgn p ≃ -1›
  have : p < 0 := lt_sgn.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ p < 0 → sgn p ≃ -1
Tactic:
intro (_ : p < 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < 0
⊢ sgn p ≃ -1
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < 0
⊢ sgn p ≃ -1
Tactic:
calc
  _ ≃ sgn p       := Rel.refl
  _ ≃ sgn (p - 0) := sgn_subst (eqv_symm sub_zero)
  _ ≃ -1          := lt_sgn.mp ‹p < 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ sgn p ≃ -1 → p < 0
Tactic:
intro (_ : sgn p ≃ -1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
⊢ p < 0
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
⊢ p < 0
Tactic:
have : sgn (p - 0) ≃ -1 := calc
  _ ≃ sgn (p - 0) := Rel.refl
  _ ≃ sgn p       := sgn_subst sub_zero
  _ ≃ -1          := ‹sgn p ≃ -1›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
this : sgn (p - 0) ≃ -1
⊢ p < 0
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
this : sgn (p - 0) ≃ -1
⊢ p < 0
Tactic:
have : p < 0 := lt_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
this✝ : sgn (p - 0) ≃ -1
this : p < 0
⊢ p < 0
Theorem: Lean4Axiomatic.Rational.lt_zero_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : sgn p ≃ -1
this✝ : sgn (p - 0) ≃ -1
this : p < 0
⊢ p < 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.gt_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p > q ↔ sgn (p - q) ≃ 1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p > q → sgn (p - q) ≃ 1

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ sgn (p - q) ≃ 1 → p > q
Theorem: Lean4Axiomatic.Rational.gt_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p > q → sgn (p - q) ≃ 1
Tactic:
case mp =>
  intro (_ : p > q)
  show sgn (p - q) ≃ 1
  have : q < p := ‹p > q›
  have : sgn (q - p) ≃ -1 := lt_sgn.mp this
  have : sgn (p - q) ≃ 1 := calc
    sgn (p - q)    ≃ _ := sgn_subst (eqv_symm neg_sub)
    sgn (-(q - p)) ≃ _ := sgn_compat_neg
    (-sgn (q - p)) ≃ _ := AA.subst₁ ‹sgn (q - p) ≃ -1›
    (-(-1))        ≃ _ := Integer.neg_involutive
    1              ≃ _ := Rel.refl
  exact this
Proof state after:
no goals