-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
    carry (i+1) x y c = atLeastTwo (x.getLsbD i) (y.getLsbD i) (carry i x y c)

Proof state:
case true.true
w i : Nat
x y : BitVec w
c : Bool
sum_bnd : x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i
⊢ decide (2 ^ i * true.toNat + x.toNat % 2 ^ i + (2 ^ i * true.toNat + y.toNat % 2 ^ i) + c.toNat ≥ 2 * 2 ^ i) =
    (true && true || true && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      true && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Tactic:
simp

Result:
case true.true
w i : Nat
x y : BitVec w
c : Bool
sum_bnd : x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i
⊢ 2 * 2 ^ i ≤ 2 ^ i + x.toNat % 2 ^ i + (2 ^ i + y.toNat % 2 ^ i) + c.toNat

Proof state:
w i : Nat
x y : BitVec w
c : Bool
⊢ carry (i + 1) x y c = (x.getLsbD i).atLeastTwo (y.getLsbD i) (carry i x y c)

Tactic:
simp only [carry, mod_two_pow_succ, atLeastTwo, getLsbD]

Result:
w i : Nat
x y : BitVec w
c : Bool
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 ^ (i + 1)) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Proof state:
w i : Nat
x y : BitVec w
c : Bool
⊢ x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 ^ i.succ

Tactic:
exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..

Result:
no goals

Proof state:
w i : Nat
x y : BitVec w
c : Bool
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 * 2 ^ i) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Tactic:
have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
  simp only [← Nat.pow_succ']
  exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..

Result:
w i : Nat
x y : BitVec w
c : Bool
sum_bnd : x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 * 2 ^ i) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Proof state:
w i : Nat
x y : BitVec w
c : Bool
sum_bnd : x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 * 2 ^ i) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Tactic:
cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)

Result:
no goals

Proof state:
w i : Nat
x y : BitVec w
c : Bool
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 ^ (i + 1)) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Tactic:
simp only [Nat.pow_succ']

Result:
w i : Nat
x y : BitVec w
c : Bool
⊢ decide
      (2 ^ i * (x.toNat.testBit i).toNat + x.toNat % 2 ^ i + (2 ^ i * (y.toNat.testBit i).toNat + y.toNat % 2 ^ i) +
          c.toNat ≥
        2 * 2 ^ i) =
    (x.toNat.testBit i && y.toNat.testBit i ||
        x.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i) ||
      y.toNat.testBit i && decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i))

Proof state:
case true.true
w i : Nat
x y : BitVec w
c : Bool
sum_bnd : x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i
⊢ 2 * 2 ^ i ≤ 2 ^ i + x.toNat % 2 ^ i + (2 ^ i + y.toNat % 2 ^ i) + c.toNat

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x y : BitVec w
c : Bool
⊢ x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 * 2 ^ i

Tactic:
simp only [← Nat.pow_succ']

Result:
w i : Nat
x y : BitVec w
c : Bool
⊢ x.toNat % 2 ^ i + (y.toNat % 2 ^ i + c.toNat) < 2 ^ i.succ