Theorem: getRes_getBit_inj_iff (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
⊢ q₁ = q₂ → getBit i q₁ = getBit i q₂ ∧ getRes i q₁ = getRes i q₂
Tactic:
rintro rfl
State after:
m : ℕ
q₁ : BV (m + 1)
i : Fin (m + 1)
⊢ getBit i q₁ = getBit i q₁ ∧ getRes i q₁ = getRes i q₁

State before:
m : ℕ
q₁ : BV (m + 1)
i : Fin (m + 1)
⊢ getBit i q₁ = getBit i q₁ ∧ getRes i q₁ = getRes i q₁
Tactic:
exact ⟨rfl, rfl⟩
State after:
no goals