case mpr =>
  intro (_ : Integer.Sqrt1 a)
  show Sqrt1 (a : ℚ)
  exact Sqrt1.from_integer eqv_refl
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
no goals