Theorem: getRes_getBit_inj (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
h₁ : getBit i q₁ = getBit i q₂
h₂ : getRes i q₁ = getRes i q₂
⊢ q₁ = q₂
Tactic:
rw [← mergeBitRes_getBit_getRes (i := i) (q := q₁), h₁, h₂, mergeBitRes_getBit_getRes]
State after:
no goals