case mp =>
  intro (_ : Sqrt1 (a : ℚ))
  show Integer.Sqrt1 a
  have (Sqrt1.from_integer_intro (b : ℤ) (_ : Integer.Sqrt1 b) eqv) :=
    ‹Sqrt1 (a : ℚ)›
  have : (b : ℚ) ≃ (a : ℚ) := eqv_symm eqv
  have : b ≃ a := from_integer_inject this
  have : Integer.Sqrt1 a := Integer.sqrt1_subst this ‹Integer.Sqrt1 b›
  exact this
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a
no goals