Theorem: getRes_condFlipBit (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getRes i ((condFlipBit i c) q) = getRes i q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h  <;> rw [condFlipBit_apply, h]
State after:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ getRes i (bif false then (flipBit i) q else q) = getRes i q

case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ getRes i (bif true then (flipBit i) q else q) = getRes i q

State before:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ getRes i (bif false then (flipBit i) q else q) = getRes i q
Tactic:
rfl
State after:
no goals

State before:
case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ getRes i (bif true then (flipBit i) q else q) = getRes i q
Tactic:
rw [cond_true, getRes_flipBit]
State after:
no goals