have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
  positive_elim_nat ‹Positive a›
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
⊢ a ≃ 1