match this with
| Or.inl (_ : Positive a) =>
  have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
  have : Sqrt1 (1:ℤ) := sqrt1_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
  exact this
| Or.inr (_ : Negative a) =>
  have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
  have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹Sqrt1 (-1:ℤ)›
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ Sqrt1 (sgn a)
no goals