case mpr =>
  intro (And.intro (_ : Sqrt1 b) (_ : a ≃ b))
  show a * b ≃ 1
  calc
    a * b ≃ _ := AA.substL ‹a ≃ b›
    b * b ≃ _ := ‹Sqrt1 b›.elim
    1     ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Sqrt1 b ∧ a ≃ b → a * b ≃ 1
no goals