case mpr =>
  intro (_ : Sqrt1 (sgn a))
  show Nonzero a
  have : sgn a ≃ 1 ∨ sgn a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 (sgn a)›
  have : Positive a ∨ Negative a := match this with
  | Or.inl (_ : sgn a ≃ 1) =>
    have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
    Or.inl this
  | Or.inr (_ : sgn a ≃ -1) =>
    have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
    Or.inr this
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr ‹Positive a ∨ Negative a›
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a
no goals