Theorem: Lean4Axiomatic.Natural.mul_positive (Lean4Axiomatic/Natural/Multiplication.lean)

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive n → Positive m → Positive (n * m)
Tactic:
intro (_ : Positive n) (_ : Positive m)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : Positive n
x✝ : Positive m
⊢ Positive (n * m)

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : Positive n
x✝ : Positive m
⊢ Positive (n * m)
Tactic:
exact mul_preserves_positive.mpr (And.intro ‹Positive n› ‹Positive m›)
State after:
no goals