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

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 ↔ p ≃ 0
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 : ℚ
⊢ -p ≃ 0 → p ≃ 0

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

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
⊢ -p ≃ 0 → p ≃ 0
Tactic:
case mp =>
  intro (_ : -p ≃ 0)
  show p ≃ 0
  calc
    p      ≃ _ := eqv_symm add_identR
    p + 0  ≃ _ := add_substR (eqv_symm ‹-p ≃ 0›)
    p + -p ≃ _ := 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 : ℚ
⊢ p ≃ 0 → -p ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ 0)
  show -p ≃ 0
  calc
    -p     ≃ _ := eqv_symm add_identL
    0 + -p ≃ _ := add_substL (eqv_symm ‹p ≃ 0›)
    p + -p ≃ _ := 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 : ℚ
⊢ -p ≃ 0 → p ≃ 0
Tactic:
intro (_ : -p ≃ 0)
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : -p ≃ 0
⊢ p ≃ 0

State before:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : -p ≃ 0
⊢ p ≃ 0
Tactic:
calc
  p      ≃ _ := eqv_symm add_identR
  p + 0  ≃ _ := add_substR (eqv_symm ‹-p ≃ 0›)
  p + -p ≃ _ := 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 : ℚ
⊢ p ≃ 0 → -p ≃ 0
Tactic:
intro (_ : p ≃ 0)
State after:
ℕ ℤ : Type
inst✝⁶ : Natural ℕ
inst✝⁵ : Integer ℤ
ℚ : Type
inst✝⁴ : Core ℚ
inst✝³ : Addition ℚ
inst✝² : Multiplication ℚ
inst✝¹ : Negation ℚ
inst✝ : Subtraction ℚ
p : ℚ
x✝ : p ≃ 0
⊢ -p ≃ 0

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