internlm/Lean-Github huggingface dataset:
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 ≤ ζ
a : ℚ
left✝ : q ≃ p + a
right✝ : abs a ≤ ε
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have (Exists.intro (b : ℚ) (And.intro (_ : s ≃ r + b) (_ : abs b ≤ δ))) :=
  close_diff ‹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
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
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✝ : r ⊢δ⊣ s
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this : ε ≥ 0
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this : ε ≥ 0
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have : s - r ≃ b := calc
  _ ≃ s - r        := eqv_refl
  _ ≃ s + -r       := sub_add_neg
  _ ≃ -r + s       := add_comm
  _ ≃ -r + (r + b) := add_substR ‹s ≃ r + b›
  _ ≃ (-r + r) + b := eqv_symm add_assoc
  _ ≃ 0 + b        := add_substL add_inverseL
  _ ≃ b            := add_identL
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝ : ε ≥ 0
this : s - r ≃ b
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝ : ε ≥ 0
this : s - r ≃ b
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b := calc
  _ ≃ q * s - p * r                := eqv_refl
  _ ≃ (p + a) * s - p * r          := sub_substL (mul_substL ‹q ≃ p + a›)
  _ ≃ p * s + a * s - p * r        := sub_substL mul_distribR
  _ ≃ p * s + a * s + (-(p * r))   := sub_add_neg
  _ ≃ p * s + (a * s + (-(p * r))) := add_assoc
  _ ≃ p * s + (-(p * r) + a * s)   := add_substR add_comm
  _ ≃ p * s + (-(p * r)) + a * s   := eqv_symm add_assoc
  _ ≃ p * s - p * r + a * s        := add_substL (eqv_symm sub_add_neg)
  _ ≃ p * (s - r) + a * s          := add_substL (eqv_symm mul_distribL_sub)
  _ ≃ p * b + a * s                := add_substL (mul_substR ‹s - r ≃ b›)
  _ ≃ p * b + a * (r + b)          := add_substR (mul_substR ‹s ≃ r + b›)
  _ ≃ p * b + (a * r + a * b)      := add_substR mul_distribL
  _ ≃ p * b + a * r + a * b        := eqv_symm add_assoc
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝ : ε ≥ 0
this : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝ : ε ≥ 0
this : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have : abs (a * r) ≤ ε * abs r := calc
  _ ≃ abs (a * r)   := eqv_refl
  _ ≃ abs a * abs r := abs_compat_mul
  _ ≤ ε * abs r     := le_substL_mul_nonneg abs_nonneg ‹abs a ≤ ε›
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝¹ : ε ≥ 0
this✝ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this : abs (a * r) ≤ ε * abs r
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝¹ : ε ≥ 0
this✝ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this : abs (a * r) ≤ ε * abs r
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have : abs (p * b) ≤ δ * abs p := calc
  _ ≃ abs (p * b)   := eqv_refl
  _ ≃ abs p * abs b := abs_compat_mul
  _ ≤ abs p * δ     := le_substR_mul_nonneg abs_nonneg ‹abs b ≤ δ›
  _ ≃ δ * abs p     := mul_comm
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have abs_ab : abs (a * b) ≤ ε * δ := calc
  _ ≃ abs (a * b)   := eqv_refl
  _ ≃ abs a * abs b := abs_compat_mul
  _ ≤ ε * abs b     := le_substL_mul_nonneg abs_nonneg ‹abs a ≤ ε›
  _ ≤ ε * δ         := le_substR_mul_nonneg ‹ε ≥ 0› ‹abs b ≤ δ›
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p := calc
  _ ≃ abs (p * b + a * r)       := eqv_refl
  _ ≤ abs (p * b) + abs (a * r) := abs_compat_add
  _ ≤ δ * abs p + abs (a * r)   := le_substL_add ‹abs (p * b) ≤ δ * abs p›
  _ ≤ δ * abs p + ε * abs r     := le_substR_add ‹abs (a * r) ≤ ε * abs r›
  _ ≃ ε * abs r + δ * abs p     := add_comm
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝² : ε ≥ 0
this✝¹ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝ : abs (a * r) ≤ ε * abs r
this : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have : dist (p * r) (q * s) ≤ ε * abs r + δ * abs p + ε * δ := calc
  _ ≃ dist (p * r) (q * s)                := eqv_refl
  _ ≃ dist (q * s) (p * r)                := dist_comm
  _ ≃ abs (q * s - p * r)                 := dist_abs
  _ ≃ abs (p * b + a * r + a * b)         := abs_subst qs_pr_eqv_pb_ar_ab
  _ ≤ abs (p * b + a * r) + abs (a * b)   := abs_compat_add
  _ ≤ ε * abs r + δ * abs p + abs (a * b) := le_substL_add abs_pb_ar
  _ ≤ ε * abs r + δ * abs p + ε * δ       := le_substR_add abs_ab
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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝³ : ε ≥ 0
this✝² : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝¹ : abs (a * r) ≤ ε * abs r
this✝ : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
this : dist (p * r) (q * s) ≤ ε * abs r + δ * abs p + ε * δ
⊢ 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 ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝³ : ε ≥ 0
this✝² : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝¹ : abs (a * r) ≤ ε * abs r
this✝ : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
this : dist (p * r) (q * s) ≤ ε * abs r + δ * abs p + ε * δ
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
Tactic:
have : p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s := 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 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 ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝⁴ : ε ≥ 0
this✝³ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝² : abs (a * r) ≤ ε * abs r
this✝¹ : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
this✝ : dist (p * r) (q * s) ≤ ε * abs r + δ * abs p + ε * δ
this : p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * 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
close_diff : ∀ {x y ζ : ℚ}, x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
a : ℚ
left✝¹ : q ≃ p + a
right✝¹ : abs a ≤ ε
b : ℚ
left✝ : s ≃ r + b
right✝ : abs b ≤ δ
this✝⁴ : ε ≥ 0
this✝³ : s - r ≃ b
qs_pr_eqv_pb_ar_ab : q * s - p * r ≃ p * b + a * r + a * b
this✝² : abs (a * r) ≤ ε * abs r
this✝¹ : abs (p * b) ≤ δ * abs p
abs_ab : abs (a * b) ≤ ε * δ
abs_pb_ar : abs (p * b + a * r) ≤ ε * abs r + δ * abs p
this✝ : dist (p * r) (q * s) ≤ ε * abs r + δ * abs p + ε * δ
this : p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
⊢ p * r ⊢ε * abs r + δ * abs p + ε * δ⊣ q * s
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 : ℚ
x✝¹ : p ⊢ε⊣ q
x✝ : r ⊢δ⊣ s
x y ζ : ℚ
⊢ x ⊢ζ⊣ y → ∃ d, y ≃ x + d ∧ abs d ≤ ζ
Tactic:
intro (_ : x ⊢ζ⊣ y)
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
Tactic:
let d := y - x
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
Tactic:
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
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
this : y ≃ x + d
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
this : y ≃ x + d
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
Tactic:
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›
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
this✝ : y ≃ x + d
this : abs d ≤ ζ
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
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
x y ζ : ℚ
x✝ : x ⊢ζ⊣ y
d : ℚ := y - x
this✝ : y ≃ x + d
this : abs d ≤ ζ
⊢ ∃ d, y ≃ x + d ∧ abs d ≤ ζ
Tactic:
exact Exists.intro d (And.intro ‹y ≃ x + d› ‹abs d ≤ ζ›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a b : Difference ℕ
⊢ a * b ≃ b * a
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * b ≃ b * a
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a * b ≃ b * a
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ n——m * b ≃ b * n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
b : Difference ℕ
n m : ℕ
⊢ n——m * b ≃ b * n——m
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, n——m * b ≃ b * n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, n——m * b ≃ b * n——m
Tactic:
intro (k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m * k——j ≃ k——j * n——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ n——m * k——j ≃ k——j * n——m
Tactic:
show (n * k + m * j)——(n * j + m * k) ≃ (k * n + j * m)——(k * m + j * n)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j)——(n * j + m * k) ≃ (k * n + j * m)——(k * m + j * n)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_comm
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j)——(n * j + m * k) ≃ (k * n + j * m)——(k * m + j * n)
Tactic:
show from_prod (n * k + m * j, n * j + m * k)
   ≃ from_prod (k * n + j * m, k * m + j * n)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ from_prod (n * k + m * j, n * j + m * k) ≃ from_prod (k * n + j * m, k * m + j * n)