internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.close_nonneg
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 → ε ≥ 0
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
⊢ ε ≥ 0
Theorem: Lean4Axiomatic.Rational.close_nonneg
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
⊢ ε ≥ 0
Tactic:
calc
  _ ≃ ε        := eqv_refl
  _ ≥ dist p q := close_dist.mp ‹p ⊢ε⊣ q›
  _ ≥ 0        := dist_nonneg
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) ↔ p ≃ q
Tactic:
apply Iff.intro
Proof 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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 → ∀ {ε : ℚ}, ε > 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
⊢ (∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q) → p ≃ q
Tactic:
intro (hyp : {ε : ℚ} → ε > 0 → 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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
⊢ p ≃ q
Tactic:
have : dist p q ≥ 0 := dist_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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this : dist p q ≥ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
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 : ℚ
hyp : ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
this✝ : dist p q ≥ 0
this : dist p q > 0 ∨ dist p q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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›
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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›
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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›
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 : ℚ
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
Theorem: Lean4Axiomatic.Rational.close_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 : ℚ
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_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 → ∀ {ε : ℚ}, ε > 0 → p ⊢ε⊣ q
Tactic:
intro (_ : p ≃ q) (ε : ℚ) (_ : ε > 0)
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
ε : ℚ
x✝ : ε > 0
⊢ p ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_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✝¹ : 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›)
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
ε : ℚ
x✝ : ε > 0
this : dist p q ≤ ε
⊢ p ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_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✝¹ : p ≃ q
ε : ℚ
x✝ : ε > 0
this : dist p q ≤ ε
⊢ p ⊢ε⊣ q
Tactic:
have : p ⊢ε⊣ q := close_dist.mpr ‹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 : ℚ
x✝¹ : p ≃ q
ε : ℚ
x✝ : ε > 0
this✝ : dist p q ≤ ε
this : p ⊢ε⊣ q
⊢ p ⊢ε⊣ q
Theorem: Lean4Axiomatic.Rational.close_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✝¹ : p ≃ q
ε : ℚ
x✝ : ε > 0
this✝ : dist p q ≤ ε
this : p ⊢ε⊣ q
⊢ p ⊢ε⊣ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_symm
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 → q ⊢ε⊣ p
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
⊢ q ⊢ε⊣ p
Theorem: Lean4Axiomatic.Rational.close_symm
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
⊢ q ⊢ε⊣ p
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 ≤ ε
⊢ q ⊢ε⊣ p
Theorem: Lean4Axiomatic.Rational.close_symm
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
this : dist p q ≤ ε
⊢ q ⊢ε⊣ p
Tactic:
have : dist q p ≤ ε := le_substL_eqv dist_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 : ℚ
x✝ : p ⊢ε⊣ q
this✝ : dist p q ≤ ε
this : dist q p ≤ ε
⊢ q ⊢ε⊣ p
Theorem: Lean4Axiomatic.Rational.close_symm
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
this✝ : dist p q ≤ ε
this : dist q p ≤ ε
⊢ q ⊢ε⊣ p
Tactic:
have : q ⊢ε⊣ p := 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✝ : p ⊢ε⊣ q
this✝¹ : dist p q ≤ ε
this✝ : dist q p ≤ ε
this : q ⊢ε⊣ p
⊢ q ⊢ε⊣ p
Theorem: Lean4Axiomatic.Rational.close_symm
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
this✝¹ : dist p q ≤ ε
this✝ : dist q p ≤ ε
this : q ⊢ε⊣ p
⊢ q ⊢ε⊣ p
Tactic:
exact this
Proof state after:
no goals
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 : ℚ
⊢ p ⊢ε⊣ q → q ⊢δ⊣ r → p ⊢ε + δ⊣ r
Tactic:
intro (_ : p ⊢ε⊣ q) (_ : 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
⊢ 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
⊢ p ⊢ε + δ⊣ 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
x✝ : q ⊢δ⊣ r
this : dist p q ≤ ε
⊢ p ⊢ε + δ⊣ r