Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_inverseL (Lean4Axiomatic/Rational/Impl/Fraction/Reciprocation.lean)

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p : Fraction ℤ
inst✝ : AP (p ≄ 0)
⊢ p⁻¹ * p ≃ 1
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ} [inst : AP (p ≄ 0)], p⁻¹ * p ≃ 1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ} [inst : AP (p ≄ 0)], p⁻¹ * p ≃ 1
Tactic:
intro (pn//pd) (_ : AP (pn//pd ≄ 0))
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Tactic:
have : Integer.Nonzero pn := nonzero_numerator (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
this : Integer.Nonzero pn
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : AP (pn//pd ≄ 0)
this : Integer.Nonzero pn
⊢ (pn//pd)⁻¹ * pn//pd ≃ 1
Tactic:
calc
  (pn//pd)⁻¹ * pn//pd
    ≃ _ := eqv_refl
  (pd * sgn pn)//(pn * sgn pn) * pn//pd
    ≃ _ := eqv_refl
  ((pd * sgn pn) * pn)//((pn * sgn pn) * pd)
    ≃ _ := substN AA.assoc
  (pd * (sgn pn * pn))//((pn * sgn pn) * pd)
    ≃ _ := substN (AA.substR AA.comm)
  (pd * (pn * sgn pn))//((pn * sgn pn) * pd)
    ≃ _ := substN AA.comm
  ((pn * sgn pn) * pd)//((pn * sgn pn) * pd)
    ≃ _ := eqv_one_iff_numer_eqv_denom.mpr Rel.refl
  1
    ≃ _ := eqv_refl
State after:
no goals