Theorem: Nat.mul_nonzero_implies_left_nonzero (MLIR/Util/KDTensor.lean)

State before:
⊢ ∀ (a b : ℕ), a * b ≠ 0 → a ≠ 0
Tactic:
intros a b NEQ
State after:
a b : ℕ
NEQ : a * b ≠ 0
⊢ a ≠ 0

State before:
a b : ℕ
NEQ : a * b ≠ 0
⊢ a ≠ 0
Tactic:
induction a
State after:
case zero
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0

case succ
b n✝ : ℕ
n_ih✝ : n✝ * b ≠ 0 → n✝ ≠ 0
NEQ : succ n✝ * b ≠ 0
⊢ succ n✝ ≠ 0

State before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0
Tactic:
case zero => {
 simp at NEQ;
}
State after:
no goals

State before:
b a' : ℕ
IH : a' * b ≠ 0 → a' ≠ 0
NEQ : succ a' * b ≠ 0
⊢ succ a' ≠ 0
Tactic:
case succ a' IH => {
  apply Nat.succ_ne_zero;
}
State after:
no goals

State before:
b : ℕ
NEQ : zero * b ≠ 0
⊢ zero ≠ 0
Tactic:
simp at NEQ
State after:
no goals

State before:
b a' : ℕ
IH : a' * b ≠ 0 → a' ≠ 0
NEQ : succ a' * b ≠ 0
⊢ succ a' ≠ 0
Tactic:
apply Nat.succ_ne_zero
State after:
no goals