Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_inverseL (Lean4Axiomatic/Rational/Impl/Fraction/Negation.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ -p + p ≃ 0
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, -p + p ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, -p + p ≃ 0
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive pd)
⊢ -pn//pd + pn//pd ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive pd)
⊢ -pn//pd + pn//pd ≃ 0
Tactic:
calc
  -(pn//pd) + pn//pd ≃ _ := eqv_refl
  (-pn)//pd + pn//pd ≃ _ := add_eqv_denominators
  (-pn + pn)//pd     ≃ _ := substN AA.inverseL
  0//pd              ≃ _ := eqv_zero_iff_numerator_eqv_zero.mpr Rel.refl
  0                  ≃ _ := eqv_refl
State after:
no goals