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

State before:
f : Bool → Bool → Bool
x : Nat
⊢ bitwise f x 0 = bif f true false then x else 0
Tactic:
rw [bitwise]
State after:
f : Bool → Bool → Bool
x : Nat
⊢ (if x = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f true false then x else 0

State before:
f : Bool → Bool → Bool
x : Nat
⊢ (if x = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bif f true false then x else 0
Tactic:
split <;> simp [*]
State after:
no goals