-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i : Nat) :
    setWidth w (x.setWidth (i + 1)) =
      setWidth w (x.setWidth i) + (x &&& twoPow w i)

Proof state:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
by_cases hik' : k < (i + 1)

Result:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : k < i + 1
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : ¬k < i + 1
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Proof state:
case pred
w : Nat
x : BitVec w
i k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x) ||| x &&& twoPow w i).getLsbD k

Tactic:
simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]

Result:
case pred
w : Nat
x : BitVec w
i k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

Proof state:
case h
w : Nat
x : BitVec w
i : Nat
⊢ setWidth w (setWidth i x) &&& (x &&& twoPow w i) = 0#w

Tactic:
ext k

Result:
case h.pred
w : Nat
x : BitVec w
i k : Nat
a✝ : k < w
⊢ (setWidth w (setWidth i x) &&& (x &&& twoPow w i)).getLsbD k = (0#w).getLsbD k

Proof state:
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : k < i + 1
⊢ k < i

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : ¬k < i + 1
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
have hik'' : ¬ (k < i) := by omega

Result:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : ¬k < i + 1
hik'' : ¬k < i
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Proof state:
case pred
w : Nat
x : BitVec w
i k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

Tactic:
by_cases hik : i = k

Result:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

Proof state:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : k < i + 1
hik'' : k < i
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
simp [hik', hik'']

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : ¬k < i + 1
⊢ ¬k < i

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

Tactic:
subst hik

Result:
case pos
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i || x.getLsbD i && (twoPow w i).getLsbD i)

Proof state:
case h.pred
w : Nat
x : BitVec w
i k : Nat
a✝ : k < w
⊢ (setWidth w (setWidth i x) &&& (x &&& twoPow w i)).getLsbD k = (0#w).getLsbD k

Tactic:
simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and,
  getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]

Result:
case h.pred
w : Nat
x : BitVec w
i k : Nat
a✝ : k < w
⊢ k < w → k < i → x.getLsbD k = true → (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD k = false

Proof state:
case h.pred
w : Nat
x : BitVec w
i k : Nat
a✝ : k < w
⊢ k < w → k < i → x.getLsbD k = true → (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD k = false

Tactic:
by_cases hi : x.getLsbD i <;> simp [hi] <;> omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| x &&& twoPow w i

Tactic:
ext k h

Result:
case pred
w : Nat
x : BitVec w
i k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x) ||| x &&& twoPow w i).getLsbD k

Proof state:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : k < i + 1
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
have hik'' : k < i := by omega

Result:
case pos
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : k < i + 1
hik'' : k < i
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i || x.getLsbD i && (twoPow w i).getLsbD i)

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
hik' : ¬k < i + 1
hik'' : ¬k < i
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
simp [hik', hik'']

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) + (x &&& twoPow w i)

Tactic:
rw [add_eq_or_of_and_eq_zero]

Result:
w : Nat
x : BitVec w
i : Nat
⊢ setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| x &&& twoPow w i

case h
w : Nat
x : BitVec w
i : Nat
⊢ setWidth w (setWidth i x) &&& (x &&& twoPow w i) = 0#w

Proof state:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k || x.getLsbD k && (twoPow w i).getLsbD k)

Tactic:
simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]

Result:
case neg
w : Nat
x : BitVec w
i k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)