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