Theorem: getBit_condFlipBit_of_ne (Controlbits/BitResiduum.lean)

State before:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i ((condFlipBit j c) q) = getBit i q
Tactic:
rw [condFlipBit_apply]
State after:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i (bif c (getRes j q) then (flipBit j) q else q) = getBit i q

State before:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i (bif c (getRes j q) then (flipBit j) q else q) = getBit i q
Tactic:
rcases (c (getRes j q)).dichotomy with (h | h) <;> simp_rw [h]
State after:
case inl
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = false
⊢ getBit i (bif false then (flipBit j) q else q) = getBit i q

case inr
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = true
⊢ getBit i (bif true then (flipBit j) q else q) = getBit i q

State before:
case inl
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = false
⊢ getBit i (bif false then (flipBit j) q else q) = getBit i q
Tactic:
rw [cond_false]
State after:
no goals

State before:
case inr
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = true
⊢ getBit i (bif true then (flipBit j) q else q) = getBit i q
Tactic:
rw [cond_true, getBit_flipBit_of_ne hij]
State after:
no goals