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

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

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

State before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
⊢ (if f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true then bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) + 1
    else bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2)) =
    2 * bitwise f (x / 2) (y / 2) + bif f (decide (x % 2 = 1)) (decide (y % 2 = 1)) then 1 else 0
Tactic:
split <;> simp [*, Nat.two_mul]
State after:
no goals