case mpr =>
  intro (_ : pn ≃ pd)
  show pn//pd ≃ 1
  show pn//pd ≃ 1//1
  show pn * 1 ≃ 1 * pd
  calc
    pn * 1 ≃ _ := AA.substL ‹pn ≃ pd›
    pd * 1 ≃ _ := AA.comm
    1 * pd ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ (pn//pd).denominator → pn//pd ≃ 1
no goals