match this with
| Or.inl (_ : s₁ ≃ s₂) =>
  exact ‹s₁ ≃ s₂›
| Or.inr (And.intro (_ : NonzeroWithSign a 1) (_ : NonzeroWithSign a (-1))) =>
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  have : Positive a ∧ Negative a := And.intro ‹Positive a› ‹Negative a›
  exact absurd ‹Positive a ∧ Negative a› not_positive_and_negative
ℕ : 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₂
no goals