internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.between_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 s t : ℚ
x✝² : p⊣ q ⊢t
x✝¹ : p⊣ s ⊢t
x✝ : q⊣ r ⊢s
left✝² : Ordered.min p t ≤ q
right✝² : q ≤ Ordered.max p t
left✝¹ : Ordered.min p t ≤ s
right✝¹ : s ≤ Ordered.max p t
left✝ : Ordered.min q s ≤ r
right✝ : r ≤ Ordered.max q s
this✝² : Ordered.min p t ≤ Ordered.min q s
this✝¹ : Ordered.max q s ≤ Ordered.max p t
this✝ : Ordered.min p t ≤ r
this : r ≤ Ordered.max p t
⊢ p⊣ r ⊢t
Tactic:
have : min p t ≤ r ∧ r ≤ max p t := And.intro ‹min p t ≤ r› ‹r ≤ max p t›
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 s t : ℚ
x✝² : p⊣ q ⊢t
x✝¹ : p⊣ s ⊢t
x✝ : q⊣ r ⊢s
left✝² : Ordered.min p t ≤ q
right✝² : q ≤ Ordered.max p t
left✝¹ : Ordered.min p t ≤ s
right✝¹ : s ≤ Ordered.max p t
left✝ : Ordered.min q s ≤ r
right✝ : r ≤ Ordered.max q s
this✝³ : Ordered.min p t ≤ Ordered.min q s
this✝² : Ordered.max q s ≤ Ordered.max p t
this✝¹ : Ordered.min p t ≤ r
this✝ : r ≤ Ordered.max p t
this : Ordered.min p t ≤ r ∧ r ≤ Ordered.max p t
⊢ p⊣ r ⊢t
Theorem: Lean4Axiomatic.Rational.between_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 s t : ℚ
x✝² : p⊣ q ⊢t
x✝¹ : p⊣ s ⊢t
x✝ : q⊣ r ⊢s
left✝² : Ordered.min p t ≤ q
right✝² : q ≤ Ordered.max p t
left✝¹ : Ordered.min p t ≤ s
right✝¹ : s ≤ Ordered.max p t
left✝ : Ordered.min q s ≤ r
right✝ : r ≤ Ordered.max q s
this✝³ : Ordered.min p t ≤ Ordered.min q s
this✝² : Ordered.max q s ≤ Ordered.max p t
this✝¹ : Ordered.min p t ≤ r
this✝ : r ≤ Ordered.max p t
this : Ordered.min p t ≤ r ∧ r ≤ Ordered.max p t
⊢ p⊣ r ⊢t
Tactic:
have : p⊣ r ⊢t := between_min_max.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 s t : ℚ
x✝² : p⊣ q ⊢t
x✝¹ : p⊣ s ⊢t
x✝ : q⊣ r ⊢s
left✝² : Ordered.min p t ≤ q
right✝² : q ≤ Ordered.max p t
left✝¹ : Ordered.min p t ≤ s
right✝¹ : s ≤ Ordered.max p t
left✝ : Ordered.min q s ≤ r
right✝ : r ≤ Ordered.max q s
this✝⁴ : Ordered.min p t ≤ Ordered.min q s
this✝³ : Ordered.max q s ≤ Ordered.max p t
this✝² : Ordered.min p t ≤ r
this✝¹ : r ≤ Ordered.max p t
this✝ : Ordered.min p t ≤ r ∧ r ≤ Ordered.max p t
this : p⊣ r ⊢t
⊢ p⊣ r ⊢t
Theorem: Lean4Axiomatic.Rational.between_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 s t : ℚ
x✝² : p⊣ q ⊢t
x✝¹ : p⊣ s ⊢t
x✝ : q⊣ r ⊢s
left✝² : Ordered.min p t ≤ q
right✝² : q ≤ Ordered.max p t
left✝¹ : Ordered.min p t ≤ s
right✝¹ : s ≤ Ordered.max p t
left✝ : Ordered.min q s ≤ r
right✝ : r ≤ Ordered.max q s
this✝⁴ : Ordered.min p t ≤ Ordered.min q s
this✝³ : Ordered.max q s ≤ Ordered.max p t
this✝² : Ordered.min p t ≤ r
this✝¹ : r ≤ Ordered.max p t
this✝ : Ordered.min p t ≤ r ∧ r ≤ Ordered.max p t
this : p⊣ r ⊢t
⊢ p⊣ r ⊢t
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
⊢ p ⊢ε⊣ q → p ⊢ε⊣ s → q⊣ r ⊢s → p ⊢ε⊣ r
Tactic:
intro (_ : p ⊢ε⊣ q) (_ : p ⊢ε⊣ s) (_ : q⊣ r ⊢s)
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
⊢ p ⊢ε⊣ r
Tactic:
have : ε ≥ 0 := close_nonneg ‹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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this : ε ≥ 0
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this : ε ≥ 0
⊢ p ⊢ε⊣ r
Tactic:
have : p-ε⊣ q ⊢p+ε := between_from_close ‹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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝ : ε ≥ 0
this : p - ε⊣ q ⊢p + ε
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝ : ε ≥ 0
this : p - ε⊣ q ⊢p + ε
⊢ p ⊢ε⊣ r
Tactic:
have : p-ε⊣ s ⊢p+ε := between_from_close ‹p ⊢ε⊣ s›
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝¹ : ε ≥ 0
this✝ : p - ε⊣ q ⊢p + ε
this : p - ε⊣ s ⊢p + ε
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝¹ : ε ≥ 0
this✝ : p - ε⊣ q ⊢p + ε
this : p - ε⊣ s ⊢p + ε
⊢ p ⊢ε⊣ r
Tactic:
have : p-ε⊣ r ⊢p+ε := between_trans ‹p-ε⊣ q ⊢p+ε› ‹p-ε⊣ s ⊢p+ε› ‹q⊣ r ⊢s›
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝² : ε ≥ 0
this✝¹ : p - ε⊣ q ⊢p + ε
this✝ : p - ε⊣ s ⊢p + ε
this : p - ε⊣ r ⊢p + ε
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝² : ε ≥ 0
this✝¹ : p - ε⊣ q ⊢p + ε
this✝ : p - ε⊣ s ⊢p + ε
this : p - ε⊣ r ⊢p + ε
⊢ p ⊢ε⊣ r
Tactic:
have : p ⊢ε⊣ r := close_from_between ‹ε ≥ 0› ‹p-ε⊣ r ⊢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 q r s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝³ : ε ≥ 0
this✝² : p - ε⊣ q ⊢p + ε
this✝¹ : p - ε⊣ s ⊢p + ε
this✝ : p - ε⊣ r ⊢p + ε
this : p ⊢ε⊣ r
⊢ p ⊢ε⊣ r
Theorem: Lean4Axiomatic.Rational.between_preserves_close
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 s : ℚ
x✝² : p ⊢ε⊣ q
x✝¹ : p ⊢ε⊣ s
x✝ : q⊣ r ⊢s
this✝³ : ε ≥ 0
this✝² : p - ε⊣ q ⊢p + ε
this✝¹ : p - ε⊣ s ⊢p + ε
this✝ : p - ε⊣ r ⊢p + ε
this : p ⊢ε⊣ r
⊢ p ⊢ε⊣ r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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 ⊢ε * abs 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 ⊢ε * abs r⊣ q * r
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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 ⊢ε * abs 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 ⊢ε * abs r⊣ q * r
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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 ⊢ε * abs r⊣ q * r
Tactic:
have : abs r ≥ 0 := abs_nonneg
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 : abs r ≥ 0
⊢ p * r ⊢ε * abs r⊣ q * r
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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 : abs r ≥ 0
⊢ p * r ⊢ε * abs r⊣ q * r
Tactic:
have : dist (p * r) (q * r) ≤ ε * abs r := calc
  _ ≃ dist (p * r) (q * r) := eqv_refl
  _ ≃ dist p q * abs r     := eqv_symm dist_distribR
  _ ≤ ε * abs r            := le_substL_mul_nonneg this ‹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✝ : abs r ≥ 0
this : dist (p * r) (q * r) ≤ ε * abs r
⊢ p * r ⊢ε * abs r⊣ q * r
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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✝ : abs r ≥ 0
this : dist (p * r) (q * r) ≤ ε * abs r
⊢ p * r ⊢ε * abs r⊣ q * r
Tactic:
have : p * r ⊢ε * abs 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✝¹ : abs r ≥ 0
this✝ : dist (p * r) (q * r) ≤ ε * abs r
this : p * r ⊢ε * abs r⊣ q * r
⊢ p * r ⊢ε * abs r⊣ q * r
Theorem: Lean4Axiomatic.Rational.close_substL_mul
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✝¹ : abs r ≥ 0
this✝ : dist (p * r) (q * r) ≤ ε * abs r
this : p * r ⊢ε * abs r⊣ q * r
⊢ p * r ⊢ε * abs r⊣ q * r
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢abs r * ε⊣ 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 ⊢abs r * ε⊣ r * q
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢abs r * ε⊣ r * q
Tactic:
have : p * r ⊢ε * abs r⊣ q * r := close_substL_mul ‹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 ⊢ε * abs r⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢ε * abs r⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Tactic:
have : r * p ⊢ε * abs r⊣ q * r := close_substL_eqv mul_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 ⊢ε * abs r⊣ q * r
this : r * p ⊢ε * abs r⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢ε * abs r⊣ q * r
this : r * p ⊢ε * abs r⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Tactic:
have : r * p ⊢(abs r) * ε⊣ q * r := close_substM_eqv mul_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 ⊢ε * abs r⊣ q * r
this✝ : r * p ⊢ε * abs r⊣ q * r
this : r * p ⊢abs r * ε⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢ε * abs r⊣ q * r
this✝ : r * p ⊢ε * abs r⊣ q * r
this : r * p ⊢abs r * ε⊣ q * r
⊢ r * p ⊢abs r * ε⊣ r * q
Tactic:
have : r * p ⊢(abs r) * ε⊣ r * q := close_substR_eqv mul_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 ⊢ε * abs r⊣ q * r
this✝¹ : r * p ⊢ε * abs r⊣ q * r
this✝ : r * p ⊢abs r * ε⊣ q * r
this : r * p ⊢abs r * ε⊣ r * q
⊢ r * p ⊢abs r * ε⊣ r * q
Theorem: Lean4Axiomatic.Rational.close_substR_mul
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 ⊢ε * abs r⊣ q * r
this✝¹ : r * p ⊢ε * abs r⊣ q * r
this✝ : r * p ⊢abs r * ε⊣ q * r
this : r * p ⊢abs r * ε⊣ r * q
⊢ r * p ⊢abs r * ε⊣ r * q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_mul_pointwise
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 s : ℚ
⊢ p ⊢ε⊣ q → r ⊢δ⊣ s → p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
intro (_ : p ⊢ε⊣ q) (_ : r ⊢δ⊣ s)
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 s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Theorem: Lean4Axiomatic.Rational.close_mul_pointwise
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 s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have close_diff
    {x y ζ : ℚ} : x ⊢ζ⊣ y → ∃ (d : ℚ), y ≃ x + d ∧ abs d ≤ ζ
    := by
  intro (_ : x ⊢ζ⊣ y)
  show ∃ (d : ℚ), y ≃ x + d ∧ abs d ≤ ζ
  let d := y - x
  have : y ≃ x + d := calc
    _ ≃ y            := eqv_refl
    _ ≃ y + 0        := eqv_symm add_identR
    _ ≃ y + (-x + x) := add_substR (eqv_symm add_inverseL)
    _ ≃ (y + -x) + x := eqv_symm add_assoc
    _ ≃ (y - x) + x  := add_substL (eqv_symm sub_add_neg)
    _ ≃ d + x        := add_substL eqv_refl
    _ ≃ x + d        := add_comm
  have : abs d ≤ ζ := calc
    _ ≃ abs d       := eqv_refl
    _ ≃ abs (y - x) := eqv_refl
    _ ≃ dist y x    := eqv_symm dist_abs
    _ ≃ dist x y    := dist_comm
    _ ≤ ζ           := close_dist.mp ‹x ⊢ζ⊣ y›
  exact Exists.intro d (And.intro ‹y ≃ x + d› ‹abs d ≤ ζ›)
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 s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Theorem: Lean4Axiomatic.Rational.close_mul_pointwise
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 s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have (Exists.intro (a : ℚ) (And.intro (_ : q ≃ p + a) (_ : abs a ≤ ε))) :=
  close_diff ‹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 s : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝ : q ≃ p + a
right✝ : abs a ≤ ε
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s