have (And.intro (_ : Positive n) (_ : Positive m)) :=
  mul_preserves_positive.mp this
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
⊢ n ≃ 1 ∧ m ≃ 1
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
⊢ n ≃ 1 ∧ m ≃ 1