case mpr =>
  intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
  show Positive x
  apply Impl.sign_props.positive_iff_sign_pos1.mpr
  show Integer.NonzeroWithSign x 1
  apply Integer.NonzeroWithSign.intro n ‹Positive n›
  show x ≃ 1 * coe n
  exact Rel.trans ‹x ≃ coe n› (Rel.symm AA.identL)
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
no goals