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

State before:
a b : Nat
⊢ a * b = zero ↔ a = zero ∨ b = zero
Tactic:
constructor
State after:
case mp
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero

case mpr
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero

State before:
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero
Tactic:
case mp =>
  intro
  apply eq_zero_or_eq_zero_of_mul_eq_zero
  assumption
State after:
no goals

State before:
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero
Tactic:
case mpr =>
  intro
  | Or.inl ha => rw [ha, zero_mul]
  | Or.inr hb => rw [hb, mul_zero]
State after:
no goals

State before:
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero
Tactic:
intro
State after:
a b : Nat
a✝ : a * b = zero
⊢ a = zero ∨ b = zero

State before:
a b : Nat
a✝ : a * b = zero
⊢ a = zero ∨ b = zero
Tactic:
apply eq_zero_or_eq_zero_of_mul_eq_zero
State after:
case x
a b : Nat
a✝ : a * b = zero
⊢ a * b = zero

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

State before:
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero
Tactic:
intro
| Or.inl ha => rw [ha, zero_mul]
| Or.inr hb => rw [hb, mul_zero]
State after:
no goals

State before:
a b : Nat
x✝ : a = zero ∨ b = zero
ha : a = zero
⊢ a * b = zero
Tactic:
rw [ha, zero_mul]
State after:
no goals

State before:
a b : Nat
x✝ : a = zero ∨ b = zero
hb : b = zero
⊢ a * b = zero
Tactic:
rw [hb, mul_zero]
State after:
no goals