exact Nonzero.mk ‹NonzeroWithSign a₂ s›
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this✝ : NonzeroWithSign a₁ s
this : NonzeroWithSign a₂ s
⊢ Nonzero a₂
no goals