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