Theorem: MyNat.mul_pos (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a ≠ zero → b ≠ zero → a * b ≠ zero
Tactic:
intro ha hb hab
State after:
a b : Nat
ha : a ≠ zero
hb : b ≠ zero
hab : a * b = zero
⊢ False

State before:
a b : Nat
ha : a ≠ zero
hb : b ≠ zero
hab : a * b = zero
⊢ False
Tactic:
cases a with
| zero => exact ha (Eq.refl zero)  | succ a' =>
  rw [succ_mul] at hab
  have hbz : b = 0 := add_left_eq_zero hab
  exact hb hbz
State after:
no goals

State before:
case zero
b : Nat
hb : b ≠ zero
ha : zero ≠ zero
hab : zero * b = zero
⊢ False
Tactic:
exact ha (Eq.refl zero)
State after:
no goals

State before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : succ a' * b = zero
⊢ False
Tactic:
rw [succ_mul] at hab
State after:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False

State before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False
Tactic:
have hbz : b = 0 := add_left_eq_zero hab
State after:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
hbz : b = 0
⊢ False

State before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
hbz : b = 0
⊢ False
Tactic:
exact hb hbz
State after:
no goals