-- 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 zero
f : Bool → Bool → Bool
x y : Nat
left : x < 2 ^ 0
right : y < 2 ^ 0
⊢ bitwise f x y < 2 ^ 0

Tactic:
simp only [eq_0_of_lt] at left right

Result:
case zero
f : Bool → Bool → Bool
x y : Nat
left : x = 0
right : y = 0
⊢ bitwise f x y < 2 ^ 0

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 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, y_zero, if_neg]

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
⊢ (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:
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 0 else 0 else if f true false = true then x else 0) < 2 ^ (n + 1)

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

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) + 1) < 2 ^ n + 2 ^ n

Tactic:
apply lt_of_succ_le

Result:
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) + (bitwise f (x / 2) (y / 2) + 1)).succ ≤ 2 ^ n + 2 ^ n

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)
⊢ (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 x_zero : x = 0 then
  simp only [x_zero, if_pos]
  by_cases p : f false true = true <;> simp [p, right]
else 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

Proof state:
x n y : Nat
f : Bool → Bool → Bool
left : x < 2 ^ n
right : y < 2 ^ n
⊢ bitwise f x y < 2 ^ n

Tactic:
induction n generalizing x y with
| zero =>
  simp only [eq_0_of_lt] at left right
  unfold bitwise
  simp [left, right]
| succ n hyp =>
  unfold bitwise
  if x_zero : x = 0 then
    simp only [x_zero, if_pos]
    by_cases p : f false true = true <;> simp [p, right]
  else 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

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) + (bitwise f (x / 2) (y / 2) + 1)).succ ≤ 2 ^ n + 2 ^ n

Tactic:
simp only [← Nat.succ_add]

Result:
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

Proof state:
case zero
f : Bool → Bool → Bool
x y : Nat
left : x = 0
right : y = 0
⊢ bitwise f x y < 2 ^ 0

Tactic:
unfold bitwise

Result:
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

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
⊢ (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:
by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
  simp [p, Nat.pow_succ, mul_succ, Nat.add_assoc]

Result:
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