case mp =>
  intro (_ : Positive (n * m))
  show Positive n ∧ Positive m
  have : n * m ≄ 0 := positive_defn.mp ‹Positive (n * m)›
  have : ¬(n ≃ 0 ∨ m ≃ 0) := mt mul_split_zero.mpr this
  have (And.intro (_ : n ≄ 0) (_ : m ≄ 0)) :=
    Logic.not_or_iff_and_not.mp this
  have : Positive n := positive_defn.mpr ‹n ≄ 0›
  have : Positive m := positive_defn.mpr ‹m ≄ 0›
  exact And.intro ‹Positive n› ‹Positive m›
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive (n * m) → Positive n ∧ Positive m
no goals