have : p₂ ≃ (a : ℚ) := AA.substLFn ‹p₁ ≃ p₂› this
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p₁ ≃ from_integer a
⊢ Sqrt1 p₂
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p₁ ≃ from_integer a
this : p₂ ≃ from_integer a
⊢ Sqrt1 p₂