exact Exists.intro n (And.intro ‹Positive n› ‹a * a ≃ (n * n : ℕ)›)
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
no goals