have (Sqrt1.from_integer_intro (a : ℤ) (_ : Integer.Sqrt1 a) eqv) :=
  ‹Sqrt1 p›
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
⊢ p * p ≃ 1
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p ≃ Rational.from_integer a
⊢ p * p ≃ 1