Theorem: binary_ne_one_eq_zero (meetings/ex5.lean)

State before:
b : binary
hb : ¬b = binary.one
⊢ b = binary.zero
Tactic:
cases b
State after:
case zero
hb : ¬binary.zero = binary.one
⊢ binary.zero = binary.zero

case one
hb : ¬binary.one = binary.one
⊢ binary.one = binary.zero

State before:
case zero
hb : ¬binary.zero = binary.one
⊢ binary.zero = binary.zero
Tactic:
simp only
State after:
no goals

State before:
case one
hb : ¬binary.one = binary.one
⊢ binary.one = binary.zero
Tactic:
simp only [not_true_eq_false] at *
State after:
no goals