-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :
    testBit (2 ^ i * a + b) j =
      if j < i then
        testBit b j
      else
        testBit a (j - i)

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ decide ((2 ^ (i - j).pred.succ * a + b / 2 ^ j) % 2 = 1) =
    if True then decide (b / 2 ^ j % 2 = 1) else decide (a / 2 ^ (j - (j + (i - j).pred.succ)) % 2 = 1)

Tactic:
simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_assoc, Nat.mul_add_mod]

Result:
no goals

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ (2 ^ i * a + b).testBit j = if True then b.testBit j else a.testBit (j - i)

Tactic:
rw [i_def]

Result:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ (2 ^ (j + (i - j).pred.succ) * a + b).testBit j =
    if True then b.testBit j else a.testBit (j - (j + (i - j).pred.succ))

Proof state:
case inr
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_ge : j ≥ i
⊢ (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)

Tactic:
have j_def : j = i + (j-i) := (Nat.add_sub_cancel' j_ge).symm

Result:
case inr
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_ge : j ≥ i
j_def : j = i + (j - i)
⊢ (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
⊢ (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)

Tactic:
simp only [j_lt]

Result:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
⊢ (2 ^ i * a + b).testBit j = if True then b.testBit j else a.testBit (j - i)

Proof state:
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
⊢ i = j + (i - j).pred.succ

Tactic:
rw [succ_pred_eq_of_pos] <;> omega

Result:
no goals

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
⊢ (2 ^ i * a + b).testBit j = if True then b.testBit j else a.testBit (j - i)

Tactic:
have i_def : i = j + succ (pred (i-j)) := by
  rw [succ_pred_eq_of_pos] <;> omega

Result:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ (2 ^ i * a + b).testBit j = if True then b.testBit j else a.testBit (j - i)

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ decide ((2 ^ j * (2 ^ (i - j).pred.succ * a) + b) / 2 ^ j % 2 = 1) =
    if True then decide (b / 2 ^ j % 2 = 1) else decide (a / 2 ^ (j - (j + (i - j).pred.succ)) % 2 = 1)

Tactic:
simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]

Result:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ decide ((2 ^ (i - j).pred.succ * a + b / 2 ^ j) % 2 = 1) =
    if True then decide (b / 2 ^ j % 2 = 1) else decide (a / 2 ^ (j - (j + (i - j).pred.succ)) % 2 = 1)

Proof state:
case inr
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_ge : j ≥ i
j_def : j = i + (j - i)
⊢ (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)

Tactic:
simp only [
    testBit_to_div_mod,
    Nat.not_lt_of_le,
    j_ge,
    ite_false]

Result:
case inr
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_ge : j ≥ i
j_def : j = i + (j - i)
⊢ decide ((2 ^ i * a + b) / 2 ^ j % 2 = 1) = decide (a / 2 ^ (j - i) % 2 = 1)

Proof state:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ (2 ^ (j + (i - j).pred.succ) * a + b).testBit j =
    if True then b.testBit j else a.testBit (j - (j + (i - j).pred.succ))

Tactic:
simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]

Result:
case inl
a b i : Nat
b_lt : b < 2 ^ i
j : Nat
j_lt : j < i
i_def : i = j + (i - j).pred.succ
⊢ decide ((2 ^ j * (2 ^ (i - j).pred.succ * a) + b) / 2 ^ j % 2 = 1) =
    if True then decide (b / 2 ^ j % 2 = 1) else decide (a / 2 ^ (j - (j + (i - j).pred.succ)) % 2 = 1)