Theorem: Nat.bit1_bitwise_bit1 (Extra/Nat/Bitwise.lean)

State before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f (2 * x + 1) (2 * y + 1) = 2 * bitwise f x y + bif f true true then 1 else 0
Tactic:
simp [pos_bitwise_pos]
State after:
no goals