Theorem: eq_flipBit_iff (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1)
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
⊢ q = (flipBit i) r ↔ getBit i q = !getBit i r ∧ getRes i q = getRes i r
Tactic:
rcases mergeBitRes_surj i q with ⟨bq, pq, rfl⟩
State after:
case intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) r ↔
    getBit i (mergeBitRes i bq pq) = !getBit i r ∧ getRes i (mergeBitRes i bq pq) = getRes i r

State before:
case intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) r ↔
    getBit i (mergeBitRes i bq pq) = !getBit i r ∧ getRes i (mergeBitRes i bq pq) = getRes i r
Tactic:
rcases mergeBitRes_surj i r with ⟨br, pr, rfl⟩
State after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) (mergeBitRes i br pr) ↔
    getBit i (mergeBitRes i bq pq) = !getBit i (mergeBitRes i br pr) ∧
      getRes i (mergeBitRes i bq pq) = getRes i (mergeBitRes i br pr)

State before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) (mergeBitRes i br pr) ↔
    getBit i (mergeBitRes i bq pq) = !getBit i (mergeBitRes i br pr) ∧
      getRes i (mergeBitRes i bq pq) = getRes i (mergeBitRes i br pr)
Tactic:
simp_rw [flipBit_mergeBitRes, getBit_mergeBitRes, getRes_mergeBitRes,
  mergeBitRes_inj_iff]
State after:
no goals