Theorem: Lean4Axiomatic.Rational.close_mul_pointwise (Lean4Axiomatic/Rational/Metric.lean)

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)
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

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 ≤ ζ›)
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

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›
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

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›
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

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›
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

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
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

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
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

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 ≤ ε›
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

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
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

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 ≤ δ›
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

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
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

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
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

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
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

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
State after:
no goals

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)
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 ≤ ζ

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
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 ≤ ζ

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
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 ≤ ζ

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›
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 ≤ ζ

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 ≤ ζ›)
State after:
no goals