Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_identL (Lean4Axiomatic/Rational/Impl/Fraction/Multiplication.lean)

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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ 1 * pn//pd ≃ pn//pd
Tactic:
calc
  1 * pn//pd         ≃ _ := eqv_refl
  1//1 * pn//pd      ≃ _ := eqv_refl
  (1 * pn)//(1 * pd) ≃ _ := substN AA.identL
  pn//(1 * pd)       ≃ _ := substD AA.identL
  pn//pd             ≃ _ := eqv_refl
State after:
no goals