Theorem: MyNat.zero_ne_one (IIScExperiments/NatAddMul.lean)

State before:
⊢ 0 ≠ 1
Tactic:
intro h
State after:
h : 0 = 1
⊢ False

State before:
h : 0 = 1
⊢ False
Tactic:
rw [← is_zero_one_eq_False]
State after:
h : 0 = 1
⊢ is_zero 1

State before:
h : 0 = 1
⊢ is_zero 1
Tactic:
rw [← h]
State after:
h : 0 = 1
⊢ is_zero 0

State before:
h : 0 = 1
⊢ is_zero 0
Tactic:
rw [is_zero_zero_eq_True]
State after:
h : 0 = 1
⊢ True

State before:
h : 0 = 1
⊢ True
Tactic:
trivial
State after:
no goals