-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mod_two_pow (x j i : Nat) :
    testBit (x % 2^j) i = (decide (i < j) && testBit x i)

Proof state:
case ind
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
⊢ (x % 2 ^ j).testBit i = (decide (i < j) && x.testBit i)

Tactic:
rw [mod_eq]

Result:
case ind
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Proof state:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
⊢ x.testBit i = true → i < j

Tactic:
rcases Nat.lt_or_ge i j with i_lt_j | i_ge_j

Result:
case ind.inl.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_lt_j : i < j
⊢ x.testBit i = true → i < j

case ind.inl.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_ge_j : i ≥ j
⊢ x.testBit i = true → i < j

Proof state:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
simp [not_j_le_x]

Result:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
⊢ x.testBit i = true → i < j

Proof state:
case ind.inl.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_ge_j : i ≥ j
⊢ x.testBit i = true → i < j

Tactic:
have x_lt : x < 2^i :=
    calc x < 2^j := x_lt_j
        _ ≤ 2^i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_ge_j

Result:
case ind.inl.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_ge_j : i ≥ j
x_lt : x < 2 ^ i
⊢ x.testBit i = true → i < j

Proof state:
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
i_lt_j : ¬i < j
⊢ (decide (i < j) && y.testBit i) = (decide (i < j) && (y + 2 ^ j).testBit i)

Tactic:
simp [i_lt_j]

Result:
no goals

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then y % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
simp only [Nat.two_pow_pos, x_eq, Nat.le_add_left, true_and, ite_true]

Result:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ (y % 2 ^ j).testBit i = (decide (i < j) && (y + 2 ^ j).testBit i)

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
⊢ (y % 2 ^ j).testBit i = (decide (i < j) && (y + 2 ^ j).testBit i)

Tactic:
simp only [hyp y y_lt_x]

Result:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
⊢ (decide (i < j) && y.testBit i) = (decide (i < j) && (y + 2 ^ j).testBit i)

Proof state:
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ 0 < 2 ^ j

Tactic:
exact Nat.two_pow_pos j

Result:
no goals

Proof state:
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ y < x

Tactic:
simp only [x_eq, Nat.lt_add_right_iff_pos]

Result:
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ 0 < 2 ^ j

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
⊢ (decide (i < j) && y.testBit i) = (decide (i < j) && (y + 2 ^ j).testBit i)

Tactic:
if i_lt_j : i < j then
  rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
else
  simp [i_lt_j]

Result:
no goals

Proof state:
case ind.inl.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_lt_j : i < j
⊢ x.testBit i = true → i < j

Tactic:
simp [i_lt_j]

Result:
no goals

Proof state:
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
i_lt_j : i < j
⊢ (decide (i < j) && y.testBit i) = (decide (i < j) && (y + 2 ^ j).testBit i)

Tactic:
rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]

Result:
no goals

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
generalize y_eq : x - 2^j = y

Result:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then y % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Proof state:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
have not_j_le_x := Nat.not_le_of_gt x_lt_j

Result:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then y % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq

Result:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then y % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)