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
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝¹ : a * b * (a * b) ≃ 1
this✝ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this : b ≃ 1 ∨ b ≃ -1
⊢ Sqrt1 b ∧ a ≃ b
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 1
this✝² : a * b * (a * b) ≃ 1
this✝¹ : Sqrt1 (a * b)
left✝ : Sqrt1 a
right✝ : Sqrt1 b
this✝ : b ≃ 1 ∨ b ≃ -1
this : a ≃ b
⊢ Sqrt1 b ∧ a ≃ b