have (Exists.intro (n : ℕ) (And.intro (_ : Positive n) a_eqv)) :=
  nonzero_squared_eqv_positive_nat_squared ‹Nonzero a›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
⊢ Sqrt1 a ∧ Sqrt1 b
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝¹ : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝ : Positive n
a_eqv : a * a ≃ coe (n * n)
⊢ Sqrt1 a ∧ Sqrt1 b