-- 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
⊢ (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:
cases p : f false true <;>
  cases yi : testBit y i <;>
    simp [x_zero, p, yi, of_false_false]

Result:
no goals

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

Tactic:
have hyp_i := hyp i (Nat.le_refl (i+1))

Result:
case succ
f : Bool → Bool → Bool
of_false_false : f false false = false
x y : Nat
x_zero : ¬x = 0
y_zero : ¬y = 0
i : Nat
hyp : ∀ (m : Nat), m < i + 1 → ∀ (x y : Nat), (bitwise f x y).testBit m = f (x.testBit m) (y.testBit m)
hyp_i : ∀ (x y : Nat), (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)
⊢ (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 + 1) =
    f (x.testBit (i + 1)) (y.testBit (i + 1))

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
⊢ (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:
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 ind
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
⊢ (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)

Tactic:
unfold bitwise

Result:
case ind
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
⊢ (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)

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 f true false = true then x else 0).testBit i = f (x.testBit i) false

Tactic:
cases p : f true false <;>
  cases xi : testBit x i <;>
    simp [p, xi, of_false_false]

Result:
no goals

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

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