Theorem: mergeBitRes_getRes_cases (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
⊢ getBit i q = false ∧ mergeBitRes i false (getRes i q) = q ∨ getBit i q = true ∧ mergeBitRes i true (getRes i q) = q
Tactic:
rcases (getBit i q).dichotomy with (h | h) <;>
simp_rw [h, mergeBitRes_getRes_of_getBit_eq h, false_and, and_self]
State after:
case inl
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = false
⊢ True ∨ False

case inr
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = true
⊢ False ∨ True

State before:
case inl
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = false
⊢ True ∨ False
Tactic:
simp_rw [or_false]
State after:
no goals

State before:
case inr
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = true
⊢ False ∨ True
Tactic:
simp_rw [or_true]
State after:
no goals