-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x y) < 2^n

Proof state:
case h
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ (bitwise f (x / 2) (y / 2)).succ + (bitwise f (x / 2) (y / 2) + 1) ≤ 2 ^ n + 2 ^ n

Tactic:
apply Nat.add_le_add <;> exact hyp1

Result:
no goals

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
⊢ (if False then if f false true = true then y else 0
    else
      if False then if f true false = true then x else 0
      else
        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 ^ (n + 1)

Tactic:
have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)

Result:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
⊢ (if False then if f false true = true then y else 0
    else
      if False then if f true false = true then x else 0
      else
        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 ^ (n + 1)

Proof state:
case succ
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
⊢ bitwise f x y < 2 ^ (n + 1)

Tactic:
unfold bitwise

Result:
case succ
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
⊢ (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 ^ (n + 1)

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : x = 0
⊢ (if f false true = true then y else 0) < 2 ^ (n + 1)

Tactic:
by_cases p : f false true = true <;> simp [p, right]

Result:
no goals

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : ¬f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) < 2 ^ n + 2 ^ n

Tactic:
apply Nat.add_lt_add <;> exact hyp1

Result:
no goals

Proof state:
case zero
f : Bool → Bool → Bool
x y : Nat
left : x = 0
right : 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 ^ 0

Tactic:
simp [left, right]

Result:
no goals

Proof state:
case neg
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : ¬f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) < 2 ^ n + 2 ^ n

Tactic:
case neg =>
  apply Nat.add_lt_add <;> exact hyp1

Result:
no goals

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : x = 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 ^ (n + 1)

Tactic:
simp only [x_zero, if_pos]

Result:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : x = 0
⊢ (if f false true = true then y else 0) < 2 ^ (n + 1)

Proof state:
case pos
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ bitwise f (x / 2) (y / 2) + (bitwise f (x / 2) (y / 2) + 1) < 2 ^ n + 2 ^ n

case neg
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : ¬f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) < 2 ^ n + 2 ^ n

Tactic:
case pos =>
  apply lt_of_succ_le
  simp only [← Nat.succ_add]
  apply Nat.add_le_add <;> exact hyp1

Result:
case neg
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp1 : bitwise f (x / 2) (y / 2) < 2 ^ n
p : ¬f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true
⊢ bitwise f (x / 2) (y / 2) + bitwise f (x / 2) (y / 2) < 2 ^ n + 2 ^ n

Proof state:
f : Bool → Bool → Bool
n : Nat
hyp : ∀ {x y : Nat}, x < 2 ^ n → y < 2 ^ n → bitwise f x y < 2 ^ n
x y : Nat
left : x < 2 ^ (n + 1)
right : y < 2 ^ (n + 1)
x_zero : ¬x = 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 ^ (n + 1)

Tactic:
if y_zero : y = 0 then
simp only [x_zero, y_zero, if_neg, if_pos]
by_cases p : f true false = true <;> simp [p, left]
else
simp only [x_zero, y_zero, if_neg]
have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)
by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
simp [p, Nat.pow_succ, mul_succ, Nat.add_assoc]
case pos =>
apply lt_of_succ_le
simp only [← Nat.succ_add]
apply Nat.add_le_add <;> exact hyp1
case neg =>
apply Nat.add_lt_add <;> exact hyp1

Result:
no goals