internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.close_trans
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this : dist p q ≤ ε
⊢ p ⊢ε + δ⊣ r
Tactic:
have : dist q r ≤ δ := close_dist.mp ‹q ⊢δ⊣ r›
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝ : dist p q ≤ ε
this : dist q r ≤ δ
⊢ p ⊢ε + δ⊣ r
Theorem: Lean4Axiomatic.Rational.close_trans
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝ : dist p q ≤ ε
this : dist q r ≤ δ
⊢ p ⊢ε + δ⊣ r
Tactic:
have : dist p r ≤ ε + δ := calc
  _ ≃ dist p r            := eqv_refl
  _ ≤ dist p q + dist q r := dist_triangle
  _ ≤ ε + dist q r        := le_substL_add ‹dist p q ≤ ε›
  _ ≤ ε + δ               := le_substR_add ‹dist q r ≤ δ›
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝¹ : dist p q ≤ ε
this✝ : dist q r ≤ δ
this : dist p r ≤ ε + δ
⊢ p ⊢ε + δ⊣ r
Theorem: Lean4Axiomatic.Rational.close_trans
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝¹ : dist p q ≤ ε
this✝ : dist q r ≤ δ
this : dist p r ≤ ε + δ
⊢ p ⊢ε + δ⊣ r
Tactic:
have : p ⊢ε+δ⊣ r := close_dist.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 q r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝² : dist p q ≤ ε
this✝¹ : dist q r ≤ δ
this✝ : dist p r ≤ ε + δ
this : p ⊢ε + δ⊣ r
⊢ p ⊢ε + δ⊣ r
Theorem: Lean4Axiomatic.Rational.close_trans
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 r : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : q ⊢δ⊣ r
this✝² : dist p q ≤ ε
this✝¹ : dist q r ≤ δ
this✝ : dist p r ≤ ε + δ
this : p ⊢ε + δ⊣ r
⊢ p ⊢ε + δ⊣ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substL_eqv
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₂ q : ℚ
⊢ p₁ ≃ p₂ → p₁ ⊢ε⊣ q → p₂ ⊢ε⊣ q
Tactic:
intro (_ : p₁ ≃ 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₁ p₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
⊢ p₂ ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_substL_eqv
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₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
⊢ p₂ ⊢ε⊣ q
Tactic:
have : dist p₁ q ≤ ε := close_dist.mp ‹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₁ p₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this : dist p₁ q ≤ ε
⊢ p₂ ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_substL_eqv
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₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this : dist p₁ q ≤ ε
⊢ p₂ ⊢ε⊣ q
Tactic:
have : dist p₂ q ≤ ε := le_substL_eqv (dist_substL ‹p₁ ≃ p₂›) 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₁ p₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this✝ : dist p₁ q ≤ ε
this : dist p₂ q ≤ ε
⊢ p₂ ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_substL_eqv
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₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this✝ : dist p₁ q ≤ ε
this : dist p₂ q ≤ ε
⊢ p₂ ⊢ε⊣ q
Tactic:
have : p₂ ⊢ε⊣ q := close_dist.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₁ p₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this✝¹ : dist p₁ q ≤ ε
this✝ : dist p₂ q ≤ ε
this : p₂ ⊢ε⊣ q
⊢ p₂ ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_substL_eqv
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₂ q : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : p₁ ⊢ε⊣ q
this✝¹ : dist p₁ q ≤ ε
this✝ : dist p₂ q ≤ ε
this : p₂ ⊢ε⊣ q
⊢ p₂ ⊢ε⊣ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substM_eqv
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 : ℚ
⊢ ε₁ ≃ ε₂ → p ⊢ε₁⊣ q → p ⊢ε₂⊣ q
Tactic:
intro (_ : ε₁ ≃ ε₂) (_ : 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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
⊢ p ⊢ε₂⊣ q
Theorem: Lean4Axiomatic.Rational.close_substM_eqv
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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
⊢ p ⊢ε₂⊣ q
Tactic:
have : dist p q ≤ ε₁ := close_dist.mp ‹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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this : dist p q ≤ ε₁
⊢ p ⊢ε₂⊣ q
Theorem: Lean4Axiomatic.Rational.close_substM_eqv
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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this : dist p q ≤ ε₁
⊢ p ⊢ε₂⊣ q
Tactic:
have : dist p q ≤ ε₂ := le_substR_eqv ‹ε₁ ≃ ε₂› 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 q : ℚ
x✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this✝ : dist p q ≤ ε₁
this : dist p q ≤ ε₂
⊢ p ⊢ε₂⊣ q
Theorem: Lean4Axiomatic.Rational.close_substM_eqv
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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this✝ : dist p q ≤ ε₁
this : dist p q ≤ ε₂
⊢ p ⊢ε₂⊣ q
Tactic:
have : p ⊢ε₂⊣ q := close_dist.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 q : ℚ
x✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this✝¹ : dist p q ≤ ε₁
this✝ : dist p q ≤ ε₂
this : p ⊢ε₂⊣ q
⊢ p ⊢ε₂⊣ q
Theorem: Lean4Axiomatic.Rational.close_substM_eqv
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✝¹ : ε₁ ≃ ε₂
x✝ : p ⊢ε₁⊣ q
this✝¹ : dist p q ≤ ε₁
this✝ : dist p q ≤ ε₂
this : p ⊢ε₂⊣ q
⊢ p ⊢ε₂⊣ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substR_eqv
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₂ : ℚ
⊢ q₁ ≃ q₂ → p ⊢ε⊣ q₁ → p ⊢ε⊣ q₂
Tactic:
intro (_ : q₁ ≃ q₂) (_ : 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₁ q₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
⊢ p ⊢ε⊣ q₂
Theorem: Lean4Axiomatic.Rational.close_substR_eqv
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₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
⊢ p ⊢ε⊣ q₂
Tactic:
have : q₁ ⊢ε⊣ p := close_symm ‹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₁ q₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this : q₁ ⊢ε⊣ p
⊢ p ⊢ε⊣ q₂
Theorem: Lean4Axiomatic.Rational.close_substR_eqv
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₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this : q₁ ⊢ε⊣ p
⊢ p ⊢ε⊣ q₂
Tactic:
have : q₂ ⊢ε⊣ p := close_substL_eqv ‹q₁ ≃ q₂› 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 q₁ q₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this✝ : q₁ ⊢ε⊣ p
this : q₂ ⊢ε⊣ p
⊢ p ⊢ε⊣ q₂
Theorem: Lean4Axiomatic.Rational.close_substR_eqv
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₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this✝ : q₁ ⊢ε⊣ p
this : q₂ ⊢ε⊣ p
⊢ p ⊢ε⊣ q₂
Tactic:
have : p ⊢ε⊣ q₂ := close_symm 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 q₁ q₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this✝¹ : q₁ ⊢ε⊣ p
this✝ : q₂ ⊢ε⊣ p
this : p ⊢ε⊣ q₂
⊢ p ⊢ε⊣ q₂
Theorem: Lean4Axiomatic.Rational.close_substR_eqv
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₂ : ℚ
x✝¹ : q₁ ≃ q₂
x✝ : p ⊢ε⊣ q₁
this✝¹ : q₁ ⊢ε⊣ p
this✝ : q₂ ⊢ε⊣ p
this : p ⊢ε⊣ q₂
⊢ p ⊢ε⊣ q₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substL_add
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 r : ℚ
⊢ p ⊢ε⊣ q → p + r ⊢ε⊣ q + r
Tactic:
intro (_ : 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 r : ℚ
x✝ : p ⊢ε⊣ q
⊢ p + r ⊢ε⊣ q + r
Theorem: Lean4Axiomatic.Rational.close_substL_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
⊢ p + r ⊢ε⊣ q + r
Tactic:
have : dist p q ≤ ε := close_dist.mp ‹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 r : ℚ
x✝ : p ⊢ε⊣ q
this : dist p q ≤ ε
⊢ p + r ⊢ε⊣ q + r
Theorem: Lean4Axiomatic.Rational.close_substL_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this : dist p q ≤ ε
⊢ p + r ⊢ε⊣ q + r
Tactic:
have : dist (p + r) (q + r) ≤ ε := calc
  _ ≃ dist (p + r) (q + r) := eqv_refl
  _ ≃ dist p q             := dist_cancelR_add
  _ ≤ ε                    := ‹dist 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 r : ℚ
x✝ : p ⊢ε⊣ q
this✝ : dist p q ≤ ε
this : dist (p + r) (q + r) ≤ ε
⊢ p + r ⊢ε⊣ q + r
Theorem: Lean4Axiomatic.Rational.close_substL_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this✝ : dist p q ≤ ε
this : dist (p + r) (q + r) ≤ ε
⊢ p + r ⊢ε⊣ q + r
Tactic:
have : p + r ⊢ε⊣ q + r := close_dist.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 q r : ℚ
x✝ : p ⊢ε⊣ q
this✝¹ : dist p q ≤ ε
this✝ : dist (p + r) (q + r) ≤ ε
this : p + r ⊢ε⊣ q + r
⊢ p + r ⊢ε⊣ q + r
Theorem: Lean4Axiomatic.Rational.close_substL_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this✝¹ : dist p q ≤ ε
this✝ : dist (p + r) (q + r) ≤ ε
this : p + r ⊢ε⊣ q + r
⊢ p + r ⊢ε⊣ q + r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substR_add
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 r : ℚ
⊢ p ⊢ε⊣ q → r + p ⊢ε⊣ r + q
Tactic:
intro (_ : 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 r : ℚ
x✝ : p ⊢ε⊣ q
⊢ r + p ⊢ε⊣ r + q
Theorem: Lean4Axiomatic.Rational.close_substR_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
⊢ r + p ⊢ε⊣ r + q
Tactic:
have : p + r ⊢ε⊣ q + r := close_substL_add ‹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 r : ℚ
x✝ : p ⊢ε⊣ q
this : p + r ⊢ε⊣ q + r
⊢ r + p ⊢ε⊣ r + q
Theorem: Lean4Axiomatic.Rational.close_substR_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this : p + r ⊢ε⊣ q + r
⊢ r + p ⊢ε⊣ r + q
Tactic:
have : r + p ⊢ε⊣ q + r := close_substL_eqv add_comm 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 q r : ℚ
x✝ : p ⊢ε⊣ q
this✝ : p + r ⊢ε⊣ q + r
this : r + p ⊢ε⊣ q + r
⊢ r + p ⊢ε⊣ r + q
Theorem: Lean4Axiomatic.Rational.close_substR_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this✝ : p + r ⊢ε⊣ q + r
this : r + p ⊢ε⊣ q + r
⊢ r + p ⊢ε⊣ r + q
Tactic:
have : r + p ⊢ε⊣ r + q := close_substR_eqv add_comm 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 q r : ℚ
x✝ : p ⊢ε⊣ q
this✝¹ : p + r ⊢ε⊣ q + r
this✝ : r + p ⊢ε⊣ q + r
this : r + p ⊢ε⊣ r + q
⊢ r + p ⊢ε⊣ r + q
Theorem: Lean4Axiomatic.Rational.close_substR_add
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 r : ℚ
x✝ : p ⊢ε⊣ q
this✝¹ : p + r ⊢ε⊣ q + r
this✝ : r + p ⊢ε⊣ q + r
this : r + p ⊢ε⊣ r + q
⊢ r + p ⊢ε⊣ r + q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_subst_neg
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 : ℚ
⊢ p ⊢ε⊣ q → -p ⊢ε⊣ -q
Tactic:
intro (_ : 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✝ : p ⊢ε⊣ q
⊢ -p ⊢ε⊣ -q
Theorem: Lean4Axiomatic.Rational.close_subst_neg
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✝ : p ⊢ε⊣ q
⊢ -p ⊢ε⊣ -q
Tactic:
have : dist p q ≤ ε := close_dist.mp ‹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✝ : p ⊢ε⊣ q
this : dist p q ≤ ε
⊢ -p ⊢ε⊣ -q