Theorem: getRes_inv (Controlbits/BitResiduum.lean)

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

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

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