have : p * p ≃ 1 := calc
  p * p             ≃ _ := mul_substL ‹p ≃ (a : ℚ)›
  (a : ℚ) * p       ≃ _ := mul_substR ‹p ≃ (a : ℚ)›
  (a : ℚ) * (a : ℚ) ≃ _ := eqv_symm mul_compat_from_integer
  ((a * a : ℤ) : ℚ) ≃ _ := from_integer_subst ‹Integer.Sqrt1 a›.elim
  (1 : ℚ)           ≃ _ := eqv_refl
  1                 ≃ _ := eqv_refl
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p ≃ Rational.from_integer a
⊢ 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 this✝ : p ≃ Rational.from_integer a
this : p * p ≃ 1
⊢ p * p ≃ 1