Theorem: Lean4Axiomatic.Rational.close_eqv (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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) ↔ p ≃ q
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) → p ≃ q

case mpr
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p q : ℚ
⊢ p ≃ q → ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q

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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) → p ≃ q
Tactic:
case mp =>
  intro (hyp : {ε : ℚ} → ε > 0 → p ⊢ε⊣ q)
  show p ≃ q
  have : dist p q ≥ 0 := dist_nonneg
  have : dist p q > 0 ∨ dist p q ≃ 0 := ge_cases.mp this
  match this with
  | Or.inl (_ : dist p q > 0) =>
    let ε := dist p q
    have (And.intro (_ : ε > ε/2) (_ : ε/2 > 0)) := halve ‹ε > 0›
    have : p ⊢ε/2⊣ q := hyp ‹ε/2 > 0›
    have : dist p q ≤ ε/2 := close_dist.mp this
    have : ε ≤ ε/2 := this
    have : p ≃ q := (le_gt_false ‹ε ≤ ε/2› ‹ε > ε/2›).elim
    exact this
  | Or.inr (_ : dist p q ≃ 0) =>
    have : p ≃ q := dist_zero.mp ‹dist p q ≃ 0›
    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 : ℚ
⊢ p ≃ q → ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
Tactic:
case mpr =>
  intro (_ : p ≃ q) (ε : ℚ) (_ : ε > 0)
  show p ⊢ε⊣ q
  have : dist p q ≤ ε := calc
    _ ≃ dist p q := eqv_refl
    _ ≃ 0        := dist_zero.mpr ‹p ≃ q›
    _ ≤ ε        := le_cases.mpr (Or.inl ‹ε > 0›)
  have : p ⊢ε⊣ q := close_dist.mpr ‹dist p q ≤ ε›
  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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) → p ≃ q
Tactic:
intro (hyp : {ε : ℚ} → ε > 0 → 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
⊢ p ≃ q
Tactic:
have : dist p q ≥ 0 := dist_nonneg
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this : dist p q ≥ 0
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this : dist p q ≥ 0
⊢ p ≃ q
Tactic:
have : dist p q > 0 ∨ dist p q ≃ 0 := ge_cases.mp 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
⊢ p ≃ q
Tactic:
match this with
| Or.inl (_ : dist p q > 0) =>
  let ε := dist p q
  have (And.intro (_ : ε > ε/2) (_ : ε/2 > 0)) := halve ‹ε > 0›
  have : p ⊢ε/2⊣ q := hyp ‹ε/2 > 0›
  have : dist p q ≤ ε/2 := close_dist.mp this
  have : ε ≤ ε/2 := this
  have : p ≃ q := (le_gt_false ‹ε ≤ ε/2› ‹ε > ε/2›).elim
  exact this
| Or.inr (_ : dist p q ≃ 0) =>
  have : p ≃ q := dist_zero.mp ‹dist p q ≃ 0›
  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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
⊢ p ≃ q
Tactic:
let ε := dist 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
⊢ p ≃ q
Tactic:
have (And.intro (_ : ε > ε/2) (_ : ε/2 > 0)) := halve ‹ε > 0›
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
⊢ p ≃ q
Tactic:
have : p ⊢ε/2⊣ q := hyp ‹ε/2 > 0›
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝¹ : dist p q ≥ 0
this✝ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this : p ⊢ε / 2⊣ q
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝¹ : dist p q ≥ 0
this✝ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this : p ⊢ε / 2⊣ q
⊢ p ≃ q
Tactic:
have : dist p q ≤ ε/2 := close_dist.mp 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝² : dist p q ≥ 0
this✝¹ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝ : p ⊢ε / 2⊣ q
this : dist p q ≤ ε / 2
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝² : dist p q ≥ 0
this✝¹ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝ : p ⊢ε / 2⊣ q
this : dist p q ≤ ε / 2
⊢ p ≃ q
Tactic:
have : ε ≤ ε/2 := 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝³ : dist p q ≥ 0
this✝² : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝¹ : p ⊢ε / 2⊣ q
this✝ : dist p q ≤ ε / 2
this : ε ≤ ε / 2
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝³ : dist p q ≥ 0
this✝² : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝¹ : p ⊢ε / 2⊣ q
this✝ : dist p q ≤ ε / 2
this : ε ≤ ε / 2
⊢ p ≃ q
Tactic:
have : p ≃ q := (le_gt_false ‹ε ≤ ε/2› ‹ε > ε/2›).elim
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝⁴ : dist p q ≥ 0
this✝³ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝² : p ⊢ε / 2⊣ q
this✝¹ : dist p q ≤ ε / 2
this✝ : ε ≤ ε / 2
this : p ≃ q
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝⁴ : dist p q ≥ 0
this✝³ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q > 0
ε : ℚ := dist p q
left✝ : ε > ε / 2
right✝ : ε / 2 > 0
this✝² : p ⊢ε / 2⊣ q
this✝¹ : dist p q ≤ ε / 2
this✝ : ε ≤ ε / 2
this : p ≃ q
⊢ p ≃ q
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q ≃ 0
⊢ p ≃ q
Tactic:
have : p ≃ q := dist_zero.mp ‹dist p q ≃ 0›
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝¹ : dist p q ≥ 0
this✝ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q ≃ 0
this : p ≃ q
⊢ p ≃ q

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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝¹ : dist p q ≥ 0
this✝ : dist p q > 0 ∨ dist p q ≃ 0
h✝ : dist p q ≃ 0
this : p ≃ q
⊢ p ≃ q
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 : ℚ
⊢ p ≃ q → ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
Tactic:
intro (_ : p ≃ q) (ε : ℚ) (_ : ε > 0)
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
ε : ℚ
x✝ : ε > 0
⊢ p ⊢ε⊣ q

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
ε : ℚ
x✝ : ε > 0
⊢ p ⊢ε⊣ q
Tactic:
have : dist p q ≤ ε := calc
  _ ≃ dist p q := eqv_refl
  _ ≃ 0        := dist_zero.mpr ‹p ≃ q›
  _ ≤ ε        := le_cases.mpr (Or.inl ‹ε > 0›)
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
ε : ℚ
x✝ : ε > 0
this : dist p q ≤ ε
⊢ p ⊢ε⊣ q

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
ε : ℚ
x✝ : ε > 0
this : dist p q ≤ ε
⊢ p ⊢ε⊣ q
Tactic:
have : p ⊢ε⊣ q := close_dist.mpr ‹dist 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 : ℚ
x✝¹ : p ≃ q
ε : ℚ
x✝ : ε > 0
this✝ : dist p q ≤ ε
this : p ⊢ε⊣ q
⊢ p ⊢ε⊣ q

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
ε : ℚ
x✝ : ε > 0
this✝ : dist p q ≤ ε
this : p ⊢ε⊣ q
⊢ p ⊢ε⊣ q
Tactic:
exact this
State after:
no goals