case mpr =>
  intro (_ : a ≄ b)
  show a * b ≃ -1
  have a_cases : a ≃ 1 ∨ a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 a›
  have b_cases : b ≃ 1 ∨ b ≃ -1 := sqrt1_cases.mp ‹Sqrt1 b›
  match a_cases with
  | Or.inl (_ : a ≃ 1) =>
    match b_cases with
    | Or.inl (_ : b ≃ 1) =>
      have : a ≃ b := Rel.trans ‹a ≃ 1› (Rel.symm ‹b ≃ 1›)
      exact absurd ‹a ≃ b› ‹a ≄ b›
    | Or.inr (_ : b ≃ -1) =>
      calc
        a * b ≃ _ := AA.substL ‹a ≃ 1›
        1 * b ≃ _ := AA.identL
        b     ≃ _ := ‹b ≃ -1›
        (-1)  ≃ _ := Rel.refl
  | Or.inr (_ : a ≃ -1) =>
    match b_cases with
    | Or.inl (_ : b ≃ 1) =>
      calc
        a * b ≃ _ := AA.substR ‹b ≃ 1›
        a * 1 ≃ _ := AA.identR
        a     ≃ _ := ‹a ≃ -1›
        (-1)  ≃ _ := Rel.refl
    | Or.inr (_ : b ≃ -1) =>
      have : a ≃ b := Rel.trans ‹a ≃ -1› (Rel.symm ‹b ≃ -1›)
      exact absurd ‹a ≃ b› ‹a ≄ b›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 a
inst✝ : Sqrt1 b
⊢ a ≄ b → a * b ≃ -1
no goals