have : s₁ ≃ s₂ ∨ (NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)) :=
  match ‹s₁ ≃ 1 ∨ s₁ ≃ -1› with
  | Or.inl (_ : s₁ ≃ 1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ 1› (Rel.symm ‹s₂ ≃ 1›)
      Or.inl ‹s₁ ≃ s₂›
    | Or.inr (_ : s₂ ≃ -1) =>
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ 1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ -1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
  | Or.inr (_ : s₁ ≃ -1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ -1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ 1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
    | Or.inr (_ : s₂ ≃ -1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ -1› (Rel.symm ‹s₂ ≃ -1›)
      Or.inl ‹s₁ ≃ s₂›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝ : s₁ ≃ 1 ∨ s₁ ≃ -1
this : s₂ ≃ 1 ∨ s₂ ≃ -1
⊢ s₁ ≃ s₂
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂