Theorem: mergeBitRes_ne_inj_iff (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ ≠ mergeBitRes i b₂ p₂ ↔ b₁ ≠ b₂ ∨ p₁ ≠ p₂
Tactic:
rw [ne_eq, mergeBitRes_inj_iff, not_and_or]
State after:
no goals