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

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

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

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

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

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

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

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

case succ
a' n✝ : ℕ
n_ih✝ : (a' * n✝ ≠ 0 → n✝ ≠ 0) → succ a' * n✝ ≠ 0 → n✝ ≠ 0
IH : a' * succ n✝ ≠ 0 → succ n✝ ≠ 0
NEQ : succ a' * succ n✝ ≠ 0
⊢ succ n✝ ≠ 0

State before:
a' : ℕ
IH : a' * zero ≠ 0 → zero ≠ 0
NEQ : succ a' * zero ≠ 0
⊢ zero ≠ 0
Tactic:
case zero => {
 simp at NEQ;
}
State after:
no goals

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

State before:
a' : ℕ
IH : a' * zero ≠ 0 → zero ≠ 0
NEQ : succ a' * zero ≠ 0
⊢ zero ≠ 0
Tactic:
simp at NEQ
State after:
no goals

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