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

State before:
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0 ∨ zero = 0
Tactic:
apply Or.inl
State after:
case h
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0

State before:
case h
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0
Tactic:
rfl
State after:
no goals

State before:
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0 ∨ succ b' = 0
Tactic:
apply Or.inl
State after:
case h
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0

State before:
case h
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0
Tactic:
rfl
State after:
no goals

State before:
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ succ a' = 0 ∨ zero = 0
Tactic:
apply Or.inr
State after:
case h
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ zero = 0

State before:
case h
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ zero = 0
Tactic:
rfl
State after:
no goals

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have ha' : succ a' ≠ zero := by exact succ_ne_zero _
State after:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have hb' : succ b' ≠ zero := by exact succ_ne_zero _
State after:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have _ : succ a' * succ b' ≠ zero := by
  apply mul_pos <;> assumption
State after:
a b a' b' : Nat
x✝¹ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
x✝ : succ a' * succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0

State before:
a b a' b' : Nat
x✝¹ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
x✝ : succ a' * succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
contradiction
State after:
no goals

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
⊢ succ a' ≠ zero
Tactic:
exact succ_ne_zero _
State after:
no goals

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ b' ≠ zero
Tactic:
exact succ_ne_zero _
State after:
no goals

State before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' * succ b' ≠ zero
Tactic:
apply mul_pos <;> assumption
State after:
no goals