case mpr =>
  intro (_ : p ≃ q)
  show p/q ≃ 1
  calc
    _ ≃ p/q := eqv_refl
    _ ≃ q/q := div_substL ‹p ≃ q›
    _ ≃ 1   := div_same
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
no goals