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