Theorem: Int.mul_ge_zero (MLIR/Util/Arith.lean)

State before:
n m : ℤ
⊢ n ≥ 0 → m ≥ 0 → n * m ≥ 0
Tactic:
rw [Int.ge_zero_eq_nonneg, Int.ge_zero_eq_nonneg, Int.ge_zero_eq_nonneg]
State after:
n m : ℤ
⊢ NonNeg n → NonNeg m → NonNeg (n * m)

State before:
n m : ℤ
⊢ NonNeg n → NonNeg m → NonNeg (n * m)
Tactic:
intros hn hm
State after:
n m : ℤ
hn : NonNeg n
hm : NonNeg m
⊢ NonNeg (n * m)

State before:
n m : ℤ
hn : NonNeg n
hm : NonNeg m
⊢ NonNeg (n * m)
Tactic:
cases hn
State after:
case mk
m : ℤ
hm : NonNeg m
n✝ : ℕ
⊢ NonNeg (ofNat n✝ * m)

State before:
case mk
m : ℤ
hm : NonNeg m
n✝ : ℕ
⊢ NonNeg (ofNat n✝ * m)
Tactic:
cases hm
State after:
case mk.mk
n✝¹ n✝ : ℕ
⊢ NonNeg (ofNat n✝¹ * ofNat n✝)

State before:
case mk.mk
n✝¹ n✝ : ℕ
⊢ NonNeg (ofNat n✝¹ * ofNat n✝)
Tactic:
constructor
State after:
no goals