Theorem: binary_zero_eq_iff_one_eq (meetings/ex5.lean)

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

case one
a : binary
hb : binary.one = binary.one ↔ a = binary.one
⊢ binary.one = binary.zero ↔ a = binary.zero

State before:
case zero
a : binary
hb : binary.zero = binary.one ↔ a = binary.one
⊢ binary.zero = binary.zero ↔ a = binary.zero
Tactic:
simp only [false_iff, forall_true_left] at *
State after:
case zero
a : binary
hb : ¬a = binary.one
⊢ True ↔ a = binary.zero

State before:
case zero
a : binary
hb : ¬a = binary.one
⊢ True ↔ a = binary.zero
Tactic:
cases a
State after:
case zero.zero
hb : ¬binary.zero = binary.one
⊢ True ↔ binary.zero = binary.zero

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

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

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

State before:
case one
a : binary
hb : binary.one = binary.one ↔ a = binary.one
⊢ binary.one = binary.zero ↔ a = binary.zero
Tactic:
simp only [true_iff, false_iff] at *
State after:
case one
a : binary
hb : a = binary.one
⊢ ¬a = binary.zero

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

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

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

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