Theorem: getBit_inv (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b : Bool
q : BV (m + 1)
i : Fin (m + 1)
h : mergeBitRes i b (getRes i q) = q
⊢ getBit i q = b
Tactic:
rcases mergeBitRes_surj i q with ⟨b', p', rfl⟩
State after:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ getBit i (mergeBitRes i b' p') = b

State before:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ getBit i (mergeBitRes i b' p') = b
Tactic:
rw [getBit_mergeBitRes]
State after:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ b' = b

State before:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ b' = b
Tactic:
exact (mergeBitRes_Bool_inj i h).symm
State after:
no goals