internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
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 : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
this : abs p ≃ p ∨ abs p ≃ -p
h✝ : abs p ≃ p
⊢ abs p ≤ q
Tactic:
calc
  _ ≃ abs p := eqv_refl
  _ ≃ p     := ‹abs p ≃ p›
  _ ≤ q     := ‹p ≤ q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_upper_bound
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 : ℚ
left✝ : -q ≤ p
right✝ : p ≤ q
this : abs p ≃ p ∨ abs p ≃ -p
h✝ : abs p ≃ -p
⊢ abs p ≤ q
Tactic:
calc
  _ ≃ abs p   := eqv_refl
  _ ≃ (-p)    := ‹abs p ≃ -p›
  _ ≤ (-(-q)) := le_subst_neg ‹-q ≤ p›
  _ ≃ q       := neg_involutive
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_compat_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 : ℚ
⊢ abs (p * q) ≃ abs p * abs q
Tactic:
have : (sgn (p * q) : ℚ) ≃ (sgn p : ℚ) * (sgn q : ℚ) := calc
  _ ≃ (sgn (p * q) : ℚ)         := eqv_refl
  _ ≃ ((sgn p * sgn q : ℤ) : ℚ) := from_integer_subst sgn_compat_mul
  _ ≃ (sgn p : ℚ) * (sgn q : ℚ) := mul_compat_from_integer
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 : ℚ
this : from_integer (sgn (p * q)) ≃ from_integer (sgn p) * from_integer (sgn q)
⊢ abs (p * q) ≃ abs p * abs q
Theorem: Lean4Axiomatic.Rational.abs_compat_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 : ℚ
this : from_integer (sgn (p * q)) ≃ from_integer (sgn p) * from_integer (sgn q)
⊢ abs (p * q) ≃ abs p * abs q
Tactic:
have : abs (p * q) ≃ abs p * abs q := calc
  _ ≃ abs (p * q)                           := eqv_refl
  _ ≃ (p * q) * (sgn (p * q) : ℚ)           := abs_sgn
  _ ≃ (p * q) * ((sgn p : ℚ) * (sgn q : ℚ)) := mul_substR this
  _ ≃ (p * sgn p) * (q * sgn q)             := AA.expr_xxfxxff_lr_swap_rl
  _ ≃ abs p * (q * sgn q)                   := mul_substL (eqv_symm abs_sgn)
  _ ≃ abs p * abs q                         := mul_substR (eqv_symm abs_sgn)
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 : ℚ
this✝ : from_integer (sgn (p * q)) ≃ from_integer (sgn p) * from_integer (sgn q)
this : abs (p * q) ≃ abs p * abs q
⊢ abs (p * q) ≃ abs p * abs q
Theorem: Lean4Axiomatic.Rational.abs_compat_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 : ℚ
this✝ : from_integer (sgn (p * q)) ≃ from_integer (sgn p) * from_integer (sgn q)
this : abs (p * q) ≃ abs p * abs q
⊢ abs (p * q) ≃ abs p * abs q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_substL
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₁ p₂ q : ℚ
⊢ p₁ ≃ p₂ → dist p₁ q ≃ dist p₂ q
Tactic:
intro (_ : p₁ ≃ 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₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ dist p₁ q ≃ dist p₂ q
Theorem: Lean4Axiomatic.Rational.dist_substL
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₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ dist p₁ q ≃ dist p₂ q
Tactic:
calc
  _ ≃ dist p₁ q    := eqv_refl
  _ ≃ abs (p₁ - q) := dist_abs
  _ ≃ abs (p₂ - q) := abs_subst (sub_substL ‹p₁ ≃ p₂›)
  _ ≃ dist p₂ q    := eqv_symm dist_abs
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_substR
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₁ p₂ q : ℚ
⊢ p₁ ≃ p₂ → dist q p₁ ≃ dist q p₂
Tactic:
intro (_ : p₁ ≃ 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₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ dist q p₁ ≃ dist q p₂
Theorem: Lean4Axiomatic.Rational.dist_substR
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₁ p₂ q : ℚ
x✝ : p₁ ≃ p₂
⊢ dist q p₁ ≃ dist q p₂
Tactic:
calc
  _ ≃ dist q p₁    := eqv_refl
  _ ≃ abs (q - p₁) := dist_abs
  _ ≃ abs (q - p₂) := abs_subst (sub_substR ‹p₁ ≃ p₂›)
  _ ≃ dist q p₂    := eqv_symm dist_abs
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_zero
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 : ℚ
⊢ dist p q ≃ 0 ↔ 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 : ℚ
⊢ dist p q ≃ 0 → 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 → dist p q ≃ 0
Theorem: Lean4Axiomatic.Rational.dist_zero
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 : ℚ
⊢ dist p q ≃ 0 → p ≃ q
Tactic:
case mp =>
  intro (_ : dist p q ≃ 0)
  show p ≃ q
  have : abs (p - q) ≃ 0 := AA.eqv_substL dist_abs ‹dist p q ≃ 0›
  have : p - q ≃ 0 := abs_zero.mp this
  have : p ≃ q := sub_eqv_zero_iff_eqv.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_zero
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 → dist p q ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show dist p q ≃ 0
  calc
    _ ≃ dist p q    := eqv_refl
    _ ≃ abs (p - q) := dist_abs
    _ ≃ abs 0       := abs_subst (sub_eqv_zero_iff_eqv.mpr ‹p ≃ q›)
    _ ≃ 0           := abs_zero.mpr eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_zero
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 : ℚ
⊢ dist p q ≃ 0 → p ≃ q
Tactic:
intro (_ : 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 : ℚ
x✝ : dist p q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.dist_zero
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✝ : dist p q ≃ 0
⊢ p ≃ q
Tactic:
have : abs (p - q) ≃ 0 := AA.eqv_substL dist_abs ‹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 : ℚ
x✝ : dist p q ≃ 0
this : abs (p - q) ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.dist_zero
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✝ : dist p q ≃ 0
this : abs (p - q) ≃ 0
⊢ p ≃ q
Tactic:
have : p - q ≃ 0 := abs_zero.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 : ℚ
x✝ : dist p q ≃ 0
this✝ : abs (p - q) ≃ 0
this : p - q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.dist_zero
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✝ : dist p q ≃ 0
this✝ : abs (p - q) ≃ 0
this : p - q ≃ 0
⊢ p ≃ q
Tactic:
have : p ≃ q := sub_eqv_zero_iff_eqv.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 : ℚ
x✝ : dist p q ≃ 0
this✝¹ : abs (p - q) ≃ 0
this✝ : p - q ≃ 0
this : p ≃ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.dist_zero
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✝ : dist p q ≃ 0
this✝¹ : abs (p - q) ≃ 0
this✝ : p - q ≃ 0
this : p ≃ q
⊢ p ≃ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.dist_zero
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 → dist 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
⊢ dist p q ≃ 0
Theorem: Lean4Axiomatic.Rational.dist_zero
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
⊢ dist p q ≃ 0
Tactic:
calc
  _ ≃ dist p q    := eqv_refl
  _ ≃ abs (p - q) := dist_abs
  _ ≃ abs 0       := abs_subst (sub_eqv_zero_iff_eqv.mpr ‹p ≃ q›)
  _ ≃ 0           := abs_zero.mpr eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ 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 : ℚ
⊢ p ⊢0⊣ 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 → p ⊢0⊣ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q → p ≃ q
Tactic:
case mp =>
  intro (_ : p ⊢0⊣ q)
  show p ≃ q
  have : dist p q ≤ 0 := close_dist.mp ‹p ⊢0⊣ q›
  have : dist p q ≥ 0 := dist_nonneg
  have : dist p q ≃ 0 := le_antisymm ‹dist p q ≤ 0› ‹dist p q ≥ 0›
  have : p ≃ q := dist_zero.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_zero
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 → p ⊢0⊣ q
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show p ⊢0⊣ q
  have : dist p q ≃ 0 := dist_zero.mpr ‹p ≃ q›
  have : dist p q ≤ 0 := le_cases.mpr (Or.inr this)
  have : p ⊢0⊣ q := close_dist.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q → p ≃ q
Tactic:
intro (_ : p ⊢0⊣ 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 ⊢0⊣ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q
⊢ p ≃ q
Tactic:
have : dist p q ≤ 0 := close_dist.mp ‹p ⊢0⊣ 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 ⊢0⊣ q
this : dist p q ≤ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q
this : dist p q ≤ 0
⊢ 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 : ℚ
x✝ : p ⊢0⊣ q
this✝ : dist p q ≤ 0
this : dist p q ≥ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q
this✝ : dist p q ≤ 0
this : dist p q ≥ 0
⊢ p ≃ q
Tactic:
have : dist p q ≃ 0 := le_antisymm ‹dist p q ≤ 0› ‹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 : ℚ
x✝ : p ⊢0⊣ q
this✝¹ : dist p q ≤ 0
this✝ : dist p q ≥ 0
this : dist p q ≃ 0
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q
this✝¹ : dist p q ≤ 0
this✝ : dist p q ≥ 0
this : dist p q ≃ 0
⊢ p ≃ q
Tactic:
have : p ≃ q := dist_zero.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 : ℚ
x✝ : p ⊢0⊣ q
this✝² : dist p q ≤ 0
this✝¹ : dist p q ≥ 0
this✝ : dist p q ≃ 0
this : p ≃ q
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ⊢0⊣ q
this✝² : dist p q ≤ 0
this✝¹ : dist p q ≥ 0
this✝ : dist p q ≃ 0
this : p ≃ q
⊢ p ≃ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.close_zero
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 → p ⊢0⊣ 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 : ℚ
x✝ : p ≃ q
⊢ p ⊢0⊣ q
Theorem: Lean4Axiomatic.Rational.close_zero
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
⊢ p ⊢0⊣ q
Tactic:
have : dist p q ≃ 0 := dist_zero.mpr ‹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 ≃ 0
⊢ p ⊢0⊣ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ≃ 0
⊢ p ⊢0⊣ q
Tactic:
have : dist p q ≤ 0 := le_cases.mpr (Or.inr 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 ≃ 0
this : dist p q ≤ 0
⊢ p ⊢0⊣ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ≃ 0
this : dist p q ≤ 0
⊢ p ⊢0⊣ q
Tactic:
have : p ⊢0⊣ q := 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 ≃ 0
this✝ : dist p q ≤ 0
this : p ⊢0⊣ q
⊢ p ⊢0⊣ q
Theorem: Lean4Axiomatic.Rational.close_zero
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 ≃ 0
this✝ : dist p q ≤ 0
this : p ⊢0⊣ q
⊢ p ⊢0⊣ q
Tactic:
exact this
Proof state after:
no goals