Theorem: Lean4Axiomatic.Rational.close_substL_sub (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 : ℚ
⊢ p ⊢ε⊣ q → p - r ⊢ε⊣ q - r
Tactic:
intro (_ : 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 : ℚ
x✝ : p ⊢ε⊣ q
⊢ p - r ⊢ε⊣ q - r

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
⊢ p - r ⊢ε⊣ q - r
Tactic:
have : p + (-r) ⊢ε⊣ q + (-r) := close_substL_add ‹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 : ℚ
x✝ : p ⊢ε⊣ q
this : p + -r ⊢ε⊣ q + -r
⊢ p - r ⊢ε⊣ q - r

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
this : p + -r ⊢ε⊣ q + -r
⊢ p - r ⊢ε⊣ q - r
Tactic:
have : p - r ⊢ε⊣ q + (-r) := close_substL_eqv (eqv_symm sub_add_neg) 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 : ℚ
x✝ : p ⊢ε⊣ q
this✝ : p + -r ⊢ε⊣ q + -r
this : p - r ⊢ε⊣ q + -r
⊢ p - r ⊢ε⊣ q - r

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
this✝ : p + -r ⊢ε⊣ q + -r
this : p - r ⊢ε⊣ q + -r
⊢ p - r ⊢ε⊣ q - r
Tactic:
have : p - r ⊢ε⊣ q - r := close_substR_eqv (eqv_symm sub_add_neg) 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 : ℚ
x✝ : p ⊢ε⊣ q
this✝¹ : p + -r ⊢ε⊣ q + -r
this✝ : p - r ⊢ε⊣ q + -r
this : p - r ⊢ε⊣ q - r
⊢ p - r ⊢ε⊣ q - r

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
this✝¹ : p + -r ⊢ε⊣ q + -r
this✝ : p - r ⊢ε⊣ q + -r
this : p - r ⊢ε⊣ q - r
⊢ p - r ⊢ε⊣ q - r
Tactic:
exact this
State after:
no goals