Theorem: getBit_flipBit_of_ne (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q : BV (m + 1)
i j : Fin (m + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
cases m
State after:
case zero
q : BV (0 + 1)
i j : Fin (0 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q

case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i j : Fin (n✝ + 1 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q

State before:
case zero
q : BV (0 + 1)
i j : Fin (0 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
exact (h ((Fin.subsingleton_one).elim i j)).elim
State after:
no goals

State before:
case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i j : Fin (n✝ + 1 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
rcases Fin.exists_succAbove_eq h with ⟨k, rfl⟩
State after:
case succ.intro
n✝ : ℕ
q : BV (n✝ + 1 + 1)
j : Fin (n✝ + 1 + 1)
k : Fin (n✝ + 1)
h : j.succAbove k ≠ j
⊢ getBit (j.succAbove k) ((flipBit j) q) = getBit (j.succAbove k) q

State before:
case succ.intro
n✝ : ℕ
q : BV (n✝ + 1 + 1)
j : Fin (n✝ + 1 + 1)
k : Fin (n✝ + 1)
h : j.succAbove k ≠ j
⊢ getBit (j.succAbove k) ((flipBit j) q) = getBit (j.succAbove k) q
Tactic:
simp_rw [getBit_succAbove, getRes_flipBit]
State after:
no goals