internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.abs_negative
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
this : from_integer (sgn p) ≃ -1
⊢ abs p ≃ -p
Tactic:
have : abs p ≃ -p := calc
  _ ≃ abs p     := eqv_refl
  _ ≃ p * sgn p := abs_sgn
  _ ≃ p * -1    := mul_substR ‹(sgn p : ℚ) ≃ -1›
  _ ≃ -1 * p    := mul_comm
  _ ≃ -p        := mul_neg_one
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
this✝ : from_integer (sgn p) ≃ -1
this : abs p ≃ -p
⊢ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_negative
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
this✝ : from_integer (sgn p) ≃ -1
this : abs p ≃ -p
⊢ abs p ≃ -p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
have : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1) := sgn_trichotomy p
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ abs p ≃ p ∨ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
match this with
| AA.OneOfThree.first (_ : sgn p ≃ 0) =>
  have : p ≃ 0 := sgn_zero.mpr ‹sgn p ≃ 0›
  have : abs p ≃ p := calc
    _ ≃ abs p := eqv_refl
    _ ≃ 0     := abs_zero.mpr ‹p ≃ 0›
    _ ≃ p     := eqv_symm ‹p ≃ 0›
  exact (Or.inl this)
| AA.OneOfThree.second (_ : sgn p ≃ 1) =>
  have : abs p ≃ p := abs_positive ‹sgn p ≃ 1›
  exact (Or.inl this)
| AA.OneOfThree.third (_ : sgn p ≃ -1) =>
  have : abs p ≃ -p := abs_negative ‹sgn p ≃ -1›
  exact (Or.inr this)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
have : p ≃ 0 := sgn_zero.mpr ‹sgn p ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this : p ≃ 0
⊢ abs p ≃ p ∨ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this : p ≃ 0
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
have : abs p ≃ p := calc
  _ ≃ abs p := eqv_refl
  _ ≃ 0     := abs_zero.mpr ‹p ≃ 0›
  _ ≃ p     := eqv_symm ‹p ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝ : p ≃ 0
this : abs p ≃ p
⊢ abs p ≃ p ∨ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
a✝ : sgn p ≃ 0
this✝ : p ≃ 0
this : abs p ≃ p
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
exact (Or.inl this)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
have : abs p ≃ p := abs_positive ‹sgn p ≃ 1›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this : abs p ≃ p
⊢ abs p ≃ p ∨ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
b✝ : sgn p ≃ 1
this : abs p ≃ p
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
exact (Or.inl this)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
have : abs p ≃ -p := abs_negative ‹sgn p ≃ -1›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this : abs p ≃ -p
⊢ abs p ≃ p ∨ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
c✝ : sgn p ≃ -1
this : abs p ≃ -p
⊢ abs p ≃ p ∨ abs p ≃ -p
Tactic:
exact (Or.inr this)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_nonneg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≥ 0
Tactic:
have : sgn (p * p) ≃ sgn (abs p) := calc
  _ ≃ sgn (p * p)   := Rel.refl
  _ ≃ sgn p * sgn p := sgn_compat_mul
  _ ≃ sgn (abs p)   := Rel.symm sgn_abs
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : sgn (p * p) ≃ sgn (abs p)
⊢ abs p ≥ 0
Theorem: Lean4Axiomatic.Rational.abs_nonneg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : sgn (p * p) ≃ sgn (abs p)
⊢ abs p ≥ 0
Tactic:
have : sgn (abs p) ≄ -1 := AA.neqv_substL this nonneg_square
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : sgn (p * p) ≃ sgn (abs p)
this : sgn (abs p) ≄ -1
⊢ abs p ≥ 0
Theorem: Lean4Axiomatic.Rational.abs_nonneg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : sgn (p * p) ≃ sgn (abs p)
this : sgn (abs p) ≄ -1
⊢ abs p ≥ 0
Tactic:
have : abs p ≥ 0 := ge_zero_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : sgn (p * p) ≃ sgn (abs p)
this✝ : sgn (abs p) ≄ -1
this : abs p ≥ 0
⊢ abs p ≥ 0
Theorem: Lean4Axiomatic.Rational.abs_nonneg
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : sgn (p * p) ≃ sgn (abs p)
this✝ : sgn (abs p) ≄ -1
this : abs p ≥ 0
⊢ abs p ≥ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_ge_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≥ p
Tactic:
show p ≤ abs p
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ p ≤ abs p
Theorem: Lean4Axiomatic.Rational.abs_ge_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ p ≤ abs p
Tactic:
calc
  _ ≃ p               := eqv_refl
  _ ≃ p * 1           := eqv_symm mul_identR
  _ ≃ p * sgn (1 : ℚ) := mul_substR (from_integer_subst (Rel.symm sgn_one))
  _ ≤ p * sgn p       := mul_sgn_self_max
  _ ≃ abs p           := eqv_symm abs_sgn
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.neg_abs_le_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ -abs p ≤ p
Tactic:
have : (sgn (-1 : ℚ) : ℚ) ≃ -1 := calc
  _ ≃ (sgn (-1 : ℚ) : ℚ) := eqv_refl
  _ ≃ ((-1 : ℤ) : ℚ)     := from_integer_subst sgn_neg_one
  _ ≃ (-1)               := neg_compat_from_integer
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : from_integer (sgn (-1)) ≃ -1
⊢ -abs p ≤ p
Theorem: Lean4Axiomatic.Rational.neg_abs_le_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this : from_integer (sgn (-1)) ≃ -1
⊢ -abs p ≤ p
Tactic:
have : -p ≤ abs p := calc
  _ ≃ -p               := eqv_refl
  _ ≃ (-1) * p         := eqv_symm mul_neg_one
  _ ≃ p * (-1)         := mul_comm
  _ ≃ p * sgn (-1 : ℚ) := mul_substR (eqv_symm this)
  _ ≤ p * sgn p        := mul_sgn_self_max
  _ ≃ abs p            := eqv_symm abs_sgn
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : from_integer (sgn (-1)) ≃ -1
this : -p ≤ abs p
⊢ -abs p ≤ p
Theorem: Lean4Axiomatic.Rational.neg_abs_le_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝ : from_integer (sgn (-1)) ≃ -1
this : -p ≤ abs p
⊢ -abs p ≤ p
Tactic:
have : -abs p ≤ p := calc
  _ ≃ -abs p := eqv_refl
  _ ≤ -(-p)  := le_subst_neg ‹-p ≤ abs p›
  _ ≃ p      := neg_involutive
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : from_integer (sgn (-1)) ≃ -1
this✝ : -p ≤ abs p
this : -abs p ≤ p
⊢ -abs p ≤ p
Theorem: Lean4Axiomatic.Rational.neg_abs_le_self
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
this✝¹ : from_integer (sgn (-1)) ≃ -1
this✝ : -p ≤ abs p
this : -abs p ≤ p
⊢ -abs p ≤ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ abs p ≤ q ↔ -q ≤ p ∧ p ≤ q
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ abs p ≤ q → -q ≤ p ∧ p ≤ q

case mpr
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ -q ≤ p ∧ p ≤ q → abs p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ abs p ≤ q → -q ≤ p ∧ p ≤ q
Tactic:
case mp =>
  intro (_ : abs p ≤ q)
  show -q ≤ p ∧ p ≤ q
  have : -q ≤ p := calc
    _ ≃ -q       := eqv_refl
    _ ≤ (-abs p) := le_subst_neg ‹abs p ≤ q›
    _ ≤ p        := neg_abs_le_self
  have : p ≤ q := calc
    _ ≃ p     := eqv_refl
    _ ≤ abs p := abs_ge_self
    _ ≤ q     := ‹abs p ≤ q›
  exact And.intro ‹-q ≤ p› ‹p ≤ q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ -q ≤ p ∧ p ≤ q → abs p ≤ q
Tactic:
case mpr =>
  intro (And.intro (_ : -q ≤ p) (_ : p ≤ q))
  show abs p ≤ q
  have : abs p ≃ p ∨ abs p ≃ -p := abs_cases
  match this with
  | Or.inl (_ : abs p ≃ p) =>
    calc
      _ ≃ abs p := eqv_refl
      _ ≃ p     := ‹abs p ≃ p›
      _ ≤ q     := ‹p ≤ q›
  | Or.inr (_ : abs p ≃ -p) =>
    calc
      _ ≃ abs p   := eqv_refl
      _ ≃ (-p)    := ‹abs p ≃ -p›
      _ ≤ (-(-q)) := le_subst_neg ‹-q ≤ p›
      _ ≃ q       := neg_involutive
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ abs p ≤ q → -q ≤ p ∧ p ≤ q
Tactic:
intro (_ : abs p ≤ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
⊢ -q ≤ p ∧ p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
⊢ -q ≤ p ∧ p ≤ q
Tactic:
have : -q ≤ p := calc
  _ ≃ -q       := eqv_refl
  _ ≤ (-abs p) := le_subst_neg ‹abs p ≤ q›
  _ ≤ p        := neg_abs_le_self
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
this : -q ≤ p
⊢ -q ≤ p ∧ p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
this : -q ≤ p
⊢ -q ≤ p ∧ p ≤ q
Tactic:
have : p ≤ q := calc
  _ ≃ p     := eqv_refl
  _ ≤ abs p := abs_ge_self
  _ ≤ q     := ‹abs p ≤ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
this✝ : -q ≤ p
this : p ≤ q
⊢ -q ≤ p ∧ p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
x✝ : abs p ≤ q
this✝ : -q ≤ p
this : p ≤ q
⊢ -q ≤ p ∧ p ≤ q
Tactic:
exact And.intro ‹-q ≤ p› ‹p ≤ q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ -q ≤ p ∧ p ≤ q → abs p ≤ q
Tactic:
intro (And.intro (_ : -q ≤ p) (_ : p ≤ q))
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
⊢ abs p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
⊢ abs p ≤ q
Tactic:
have : abs p ≃ p ∨ abs p ≃ -p := abs_cases
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
this : abs p ≃ p ∨ abs p ≃ -p
⊢ abs p ≤ q
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
this : abs p ≃ p ∨ abs p ≃ -p
⊢ abs p ≤ q
Tactic:
match this with
| Or.inl (_ : abs p ≃ p) =>
  calc
    _ ≃ abs p := eqv_refl
    _ ≃ p     := ‹abs p ≃ p›
    _ ≤ q     := ‹p ≤ q›
| Or.inr (_ : abs p ≃ -p) =>
  calc
    _ ≃ abs p   := eqv_refl
    _ ≃ (-p)    := ‹abs p ≃ -p›
    _ ≤ (-(-q)) := le_subst_neg ‹-q ≤ p›
    _ ≃ q       := neg_involutive
Proof state after:
no goals