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

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

State before:
a : ℕ
⊢ ∀ (b : ℕ), a ≠ 0 → b ≠ 0 → a * b ≠ 0
Tactic:
induction a
State after:
case zero

⊢ ∀ (b : ℕ), zero ≠ 0 → b ≠ 0 → zero * b ≠ 0

case succ
n✝ : ℕ
n_ih✝ : ∀ (b : ℕ), n✝ ≠ 0 → b ≠ 0 → n✝ * b ≠ 0
⊢ ∀ (b : ℕ), succ n✝ ≠ 0 → b ≠ 0 → succ n✝ * b ≠ 0

State before:
⊢ ∀ (b : ℕ), zero ≠ 0 → b ≠ 0 → zero * b ≠ 0
Tactic:
case zero => {
  intros b A_NEQ_ZERO; simp [A_NEQ_ZERO]; contradiction;
}
State after:
no goals

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ ∀ (b : ℕ), succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Tactic:
case succ a' IH => {
  intros b;
  induction b;
  case zero => {
     intros A B;
     simp at B;
  }
  case succ b' IH' => {
   intros A B;
   simp [Nat.mul];
 }
}
State after:
no goals

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

State before:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ b ≠ 0 → zero * b ≠ 0
Tactic:
simp [A_NEQ_ZERO]
State after:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ 0 < b → False

State before:
b : ℕ
A_NEQ_ZERO : zero ≠ 0
⊢ 0 < b → False
Tactic:
contradiction
State after:
no goals

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

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b : ℕ
⊢ succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
Tactic:
induction b
State after:
case zero
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0

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

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0
Tactic:
case zero => {
   intros A B;
   simp at B;
}
State after:
no goals

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
⊢ succ a' ≠ 0 → succ b' ≠ 0 → succ a' * succ b' ≠ 0
Tactic:
case succ b' IH' => {
 intros A B;
 simp [Nat.mul];
}
State after:
no goals

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ succ a' ≠ 0 → zero ≠ 0 → succ a' * zero ≠ 0
Tactic:
intros A B
State after:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
A : succ a' ≠ 0
B : zero ≠ 0
⊢ succ a' * zero ≠ 0

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
A : succ a' ≠ 0
B : zero ≠ 0
⊢ succ a' * zero ≠ 0
Tactic:
simp at B
State after:
no goals

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
⊢ succ a' ≠ 0 → succ b' ≠ 0 → succ a' * succ b' ≠ 0
Tactic:
intros A B
State after:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
A : succ a' ≠ 0
B : succ b' ≠ 0
⊢ succ a' * succ b' ≠ 0

State before:
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
A : succ a' ≠ 0
B : succ b' ≠ 0
⊢ succ a' * succ b' ≠ 0
Tactic:
simp [Nat.mul]
State after:
no goals