have : NonzeroWithSign a₂ s :=
  NonzeroWithSign.subst_nonzero ‹a₁ ≃ a₂› ‹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
⊢ Nonzero a₂
ℕ : 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₂