Theorem: binary'_zero_eq_iff_one_eq (meetings/ex5.lean)

State before:
b : ↑binary'
hb : ¬↑b = 1
⊢ ↑b = 0
Tactic:
rcases b with ⟨hv, hp⟩
State after:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬↑{ val := hv, property := hp } = 1
⊢ ↑{ val := hv, property := hp } = 0

State before:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬↑{ val := hv, property := hp } = 1
⊢ ↑{ val := hv, property := hp } = 0
Tactic:
dsimp only at *
State after:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬hv = 1
⊢ hv = 0

State before:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬hv = 1
⊢ hv = 0
Tactic:
rw [binary'] at hp
State after:
case mk
hv : ℕ
hp : hv ∈ {0, 1}
hb : ¬hv = 1
⊢ hv = 0

State before:
case mk
hv : ℕ
hp : hv ∈ {0, 1}
hb : ¬hv = 1
⊢ hv = 0
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hp
State after:
case mk
hv : ℕ
hb : ¬hv = 1
hp : hv = 0 ∨ hv = 1
⊢ hv = 0

State before:
case mk
hv : ℕ
hb : ¬hv = 1
hp : hv = 0 ∨ hv = 1
⊢ hv = 0
Tactic:
rcases hp with (h0 | h1)
State after:
case mk.inl
hv : ℕ
hb : ¬hv = 1
h0 : hv = 0
⊢ hv = 0

case mk.inr
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ hv = 0

State before:
case mk.inl
hv : ℕ
hb : ¬hv = 1
h0 : hv = 0
⊢ hv = 0
Tactic:
exact h0
State after:
no goals

State before:
case mk.inr
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ hv = 0
Tactic:
exfalso
State after:
case mk.inr.h
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ False

State before:
case mk.inr.h
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ False
Tactic:
exact hb h1
State after:
no goals