case mp =>
  intro (_ : Nonzero a)
  show Sqrt1 (sgn a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  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 : ℤ
⊢ Nonzero a → Sqrt1 (sgn a)
no goals