Theorem: Lean4Axiomatic.Rational.sub_eqv_zero_iff_eqv (Lean4Axiomatic/Rational/Negation.lean)

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 ↔ p ≃ q
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q

case mpr
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q
Tactic:
case mp =>
  intro (_ : p - q ≃ 0)
  show p ≃ q
  calc
    p            ≃ _ := eqv_symm add_identR
    p + 0        ≃ _ := add_substR (eqv_symm add_inverseL)
    p + (-q + q) ≃ _ := eqv_symm add_assoc
    (p + -q) + q ≃ _ := add_substL (eqv_symm sub_add_neg)
    (p - q) + q  ≃ _ := add_substL ‹p - q ≃ 0›
    0 + q        ≃ _ := add_identL
    q            ≃ _ := eqv_refl
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show p - q ≃ 0
  calc
    p - q  ≃ _ := sub_add_neg
    p + -q ≃ _ := add_substL ‹p ≃ q›
    q + -q ≃ _ := add_inverseR
    0      ≃ _ := eqv_refl
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p - q ≃ 0 → p ≃ q
Tactic:
intro (_ : p - q ≃ 0)
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p - q ≃ 0
⊢ p ≃ q

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p - q ≃ 0
⊢ p ≃ q
Tactic:
calc
  p            ≃ _ := eqv_symm add_identR
  p + 0        ≃ _ := add_substR (eqv_symm add_inverseL)
  p + (-q + q) ≃ _ := eqv_symm add_assoc
  (p + -q) + q ≃ _ := add_substL (eqv_symm sub_add_neg)
  (p - q) + q  ≃ _ := add_substL ‹p - q ≃ 0›
  0 + q        ≃ _ := add_identL
  q            ≃ _ := eqv_refl
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
⊢ p ≃ q → p - q ≃ 0
Tactic:
intro (_ : p ≃ q)
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p ≃ q
⊢ p - q ≃ 0

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p q : ℚ
x✝ : p ≃ q
⊢ p - q ≃ 0
Tactic:
calc
  p - q  ≃ _ := sub_add_neg
  p + -q ≃ _ := add_substL ‹p ≃ q›
  q + -q ≃ _ := add_inverseR
  0      ≃ _ := eqv_refl
State after:
no goals