-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j))

Proof state:
case zero
i j : Nat
⊢ (twoPow 0 i).getLsbD j = (decide (i < 0) && decide (i = j))

Tactic:
simp

Result:
no goals

Proof state:
case succ
i j w : Nat
⊢ (twoPow (w + 1) i).getLsbD j = (decide (i < w + 1) && decide (i = j))

Tactic:
simp only [twoPow, getLsbD_shiftLeft, getLsbD_ofNat]

Result:
case succ
i j w : Nat
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
hi' : j - i = 0
hij : j = i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
simp_all

Result:
no goals

Proof state:
i w : Nat
hj : ¬i < i
hi : ¬Nat.testBit 1 (i - i) = true
⊢ False

Tactic:
simp at hi

Result:
no goals

Proof state:
case neg
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
hij : i ≠ j
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
simp_all

Result:
no goals

Proof state:
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
hi' : j - i = 0
⊢ j = i

Tactic:
omega

Result:
no goals

Proof state:
case pos
i j w : Nat
hj : j < i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
simp only [hj, decide_true, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]

Result:
case pos
i j w : Nat
hj : j < i
⊢ i < w + 1 → ¬i = j

Proof state:
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
h : i = j
⊢ False

Tactic:
subst h

Result:
i w : Nat
hj : ¬i < i
hi : ¬Nat.testBit 1 (i - i) = true
⊢ False

Proof state:
case succ
i j w : Nat
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
by_cases hj : j < i

Result:
case pos
i j w : Nat
hj : j < i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

case neg
i j w : Nat
hj : ¬j < i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
case neg
i j w : Nat
hj : ¬j < i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
by_cases hi : Nat.testBit 1 (j - i)

Result:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

case neg
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
hi' : j - i = 0
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
have hij : j = i := by omega

Result:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
hi' : j - i = 0
hij : j = i
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi

Result:
case pos
i j w : Nat
hj : ¬j < i
hi : Nat.testBit 1 (j - i) = true
hi' : j - i = 0
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
case neg
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Tactic:
have hij : i ≠ j := by
  intro h; subst h
  simp at hi

Result:
case neg
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
hij : i ≠ j
⊢ (decide (j < w + 1) && !decide (j < i) && (decide (j - i < w + 1) && Nat.testBit 1 (j - i))) =
    (decide (i < w + 1) && decide (i = j))

Proof state:
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
⊢ i ≠ j

Tactic:
intro h

Result:
i j w : Nat
hj : ¬j < i
hi : ¬Nat.testBit 1 (j - i) = true
h : i = j
⊢ False

Proof state:
w i j : Nat
⊢ (twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))

Tactic:
rcases w with rfl | w

Result:
case zero
i j : Nat
⊢ (twoPow 0 i).getLsbD j = (decide (i < 0) && decide (i = j))

case succ
i j w : Nat
⊢ (twoPow (w + 1) i).getLsbD j = (decide (i < w + 1) && decide (i = j))

Proof state:
case pos
i j w : Nat
hj : j < i
⊢ i < w + 1 → ¬i = j

Tactic:
omega

Result:
no goals