case mpr =>
  intro (_ : n ≃ 1)
  show n * n ≃ 1
  have : n * n ≃ 1 := factors_eqv_1.mpr (And.intro ‹n ≃ 1› ‹n ≃ 1›)
  exact this
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
no goals