-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_bitwise (of_false_false : f false false = false) (x y i : Nat) :
    (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)

Proof state:
f : Bool → Bool → Bool
of_false_false : f false false = false
i : Nat
hyp : ∀ (m : Nat), m < i → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
x y : Nat
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).testBit
      i =
    f (x.testBit i) (y.testBit i)

Tactic:
simp only [x_zero, y_zero, ←Nat.two_mul]

Result:
f : Bool → Bool → Bool
of_false_false : f false false = false
i : Nat
hyp : ∀ (m : Nat), m < i → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
x y : Nat
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 2 * bitwise f (x / 2) (y / 2) + 1
            else 2 * bitwise f (x / 2) (y / 2)).testBit
      i =
    f (x.testBit i) (y.testBit i)

Proof state:
f : Bool → Bool → Bool
of_false_false : f false false = false
i : Nat
hyp : ∀ (m : Nat), m < i → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
x y : Nat
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).testBit
      i =
    f (x.testBit i) (y.testBit i)

Tactic:
simp [x_zero, y_zero]

Result:
f : Bool → Bool → Bool
of_false_false : f false false = false
i : Nat
hyp : ∀ (m : Nat), m < i → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
x y : Nat
x_zero : ¬x = 0
y_zero : y = 0
⊢ (if f true false = true then x else 0).testBit i = f (x.testBit i) false

Proof state:
f : Bool → Bool → Bool
of_false_false : f false false = false
i : Nat
hyp : ∀ (m : Nat), m < i → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
x y : Nat
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 2 * bitwise f (x / 2) (y / 2) + 1
            else 2 * bitwise f (x / 2) (y / 2)).testBit
      i =
    f (x.testBit i) (y.testBit i)

Tactic:
cases i with
| zero =>
  cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
    simp [p, Nat.mul_add_mod, mod_eq_of_lt]
| succ i =>
  have hyp_i := hyp i (Nat.le_refl (i+1))
  cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
    simp [p, one_div_two, hyp_i, Nat.mul_add_div]

Result:
no goals

Proof state:
f : Bool → Bool → Bool
of_false_false : f false false = false
x y i : Nat
⊢ (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)

Tactic:
induction i using Nat.strongRecOn generalizing x y with
| ind i hyp =>
  unfold bitwise
  if x_zero : x = 0 then
    cases p : f false true <;>
      cases yi : testBit y i <;>
        simp [x_zero, p, yi, of_false_false]
  else if y_zero : y = 0 then
    simp [x_zero, y_zero]
    cases p : f true false <;>
      cases xi : testBit x i <;>
        simp [p, xi, of_false_false]
  else
    simp only [x_zero, y_zero, ←Nat.two_mul]
    cases i with
    | zero =>
      cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
        simp [p, Nat.mul_add_mod, mod_eq_of_lt]
    | succ i =>
      have hyp_i := hyp i (Nat.le_refl (i+1))
      cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
        simp [p, one_div_two, hyp_i, Nat.mul_add_div]

Result:
no goals

Proof state:
case zero
f : Bool → Bool → Bool
of_false_false : f false false = false
x y : Nat
x_zero : ¬x = 0
y_zero : ¬y = 0
hyp : ∀ (m : Nat), m < 0 → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
⊢ (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 2 * bitwise f (x / 2) (y / 2) + 1
            else 2 * bitwise f (x / 2) (y / 2)).testBit
      0 =
    f (x.testBit 0) (y.testBit 0)

Tactic:
cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
  simp [p, Nat.mul_add_mod, mod_eq_of_lt]

Result:
no goals