case mp =>
  intro (_ : a * b ≃ 1)
  show Sqrt1 b ∧ a ≃ b
  have : (a * b) * (a * b) ≃ 1 := calc
    (a * b) * (a * b) ≃ _ := AA.substL ‹a * b ≃ 1›
    1 * (a * b)       ≃ _ := AA.identL
    a * b             ≃ _ := ‹a * b ≃ 1›
    1                 ≃ _ := Rel.refl
  have : Sqrt1 (a * b) := Sqrt1.mk this
  have (And.intro (_ : Sqrt1 a) (_ : Sqrt1 b)) :=
    sqrt1_factors_if_sqrt1_product this
  have : b ≃ 1 ∨ b ≃ -1 := sqrt1_cases.mp ‹Sqrt1 b›
  have : a ≃ b :=
    match this with
    | Or.inl (_ : b ≃ 1) => calc
      a     ≃ _ := Rel.symm AA.identR
      a * 1 ≃ _ := AA.substR (Rel.symm ‹b ≃ 1›)
      a * b ≃ _ := ‹a * b ≃ 1›
      1     ≃ _ := Rel.symm ‹b ≃ 1›
      b     ≃ _ := Rel.refl
    | Or.inr (_ : b ≃ -1) => calc
      a             ≃ _ := Rel.symm neg_involutive
      (-(-a))       ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
      (-(-(a * 1))) ≃ _ := AA.subst₁ AA.scompatR
      (-(a * -1))   ≃ _ := AA.subst₁ (AA.substR (Rel.symm ‹b ≃ -1›))
      (-(a * b))    ≃ _ := AA.subst₁ ‹a * b ≃ 1›
      (-1)          ≃ _ := Rel.symm ‹b ≃ -1›
      b             ≃ _ := Rel.refl
  exact And.intro ‹Sqrt1 b› ‹a ≃ b›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 1 → Sqrt1 b ∧ a ≃ b
no goals