Theorem: mergeBitRes_inj_iff (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
⊢ b₁ = b₂ ∧ p₁ = p₂ → mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
Tactic:
rintro ⟨rfl, rfl⟩
State after:
case intro
m : ℕ
b₁ : Bool
p₁ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ = mergeBitRes i b₁ p₁

State before:
case intro
m : ℕ
b₁ : Bool
p₁ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ = mergeBitRes i b₁ p₁
Tactic:
rfl
State after:
no goals