-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
    getLsbD (x + y + setWidth w (ofBool c)) i =
      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y c))

Proof state:
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ({ toFin := ⟨x, x_lt⟩ } + { toFin := ⟨y, y_lt⟩ } + setWidth w (ofBool c)).getLsbD i =
    ({ toFin := ⟨x, x_lt⟩ }.getLsbD i ^^
      ({ toFin := ⟨y, y_lt⟩ }.getLsbD i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Tactic:
simp only [getLsbD, toNat_add, toNat_setWidth, i_lt, toNat_ofFin, toNat_ofBool,
  Nat.mod_add_mod, Nat.add_mod_mod]

Result:
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((x + y + c.toNat) % 2 ^ w).testBit i =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Proof state:
case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((2 ^ i * (x / 2 ^ i) + x % 2 ^ i + (2 ^ i * (y / 2 ^ i) + y % 2 ^ i) + c.toNat) % 2 ^ w).testBit i =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Tactic:
simp only
  [ Nat.testBit_mod_two_pow,
    Nat.testBit_mul_two_pow_add_eq,
    i_lt,
    decide_true,
    Bool.true_and,
    Nat.add_assoc,
    Nat.add_left_comm (_%_) (_ * _) _,
    testBit_limit (mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ x y i c)
  ]

Result:
case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ (decide (x / 2 ^ i % 2 = 1) ^^ (decide (y / 2 ^ i % 2 = 1) ^^ decide (x % 2 ^ i + (y % 2 ^ i + c.toNat) ≥ 2 ^ i))) =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Proof state:
case h₁
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((x + y + c.toNat) % 2 ^ w).testBit i = ?b

case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ?b = (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

case b
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ Bool

Tactic:
rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]

Result:
case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((2 ^ i * (x / 2 ^ i) + x % 2 ^ i + (2 ^ i * (y / 2 ^ i) + y % 2 ^ i) + c.toNat) % 2 ^ w).testBit i =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Proof state:
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((x + y + c.toNat) % 2 ^ w).testBit i =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Tactic:
apply Eq.trans

Result:
case h₁
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ((x + y + c.toNat) % 2 ^ w).testBit i = ?b

case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ?b = (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

case b
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ Bool

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
c : Bool
⊢ (x + y + setWidth w (ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y c))

Tactic:
let ⟨x, x_lt⟩ := x

Result:
w i : Nat
i_lt : i < w
x✝ y : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
⊢ ({ toFin := ⟨x, x_lt⟩ } + y + setWidth w (ofBool c)).getLsbD i =
    ({ toFin := ⟨x, x_lt⟩ }.getLsbD i ^^ (y.getLsbD i ^^ carry i { toFin := ⟨x, x_lt⟩ } y c))

Proof state:
case h₂
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ (decide (x / 2 ^ i % 2 = 1) ^^ (decide (y / 2 ^ i % 2 = 1) ^^ decide (x % 2 ^ i + (y % 2 ^ i + c.toNat) ≥ 2 ^ i))) =
    (x.testBit i ^^ (y.testBit i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))

Tactic:
simp [testBit_to_div_mod, carry, Nat.add_assoc]

Result:
no goals

Proof state:
w i : Nat
i_lt : i < w
x✝ y : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
⊢ ({ toFin := ⟨x, x_lt⟩ } + y + setWidth w (ofBool c)).getLsbD i =
    ({ toFin := ⟨x, x_lt⟩ }.getLsbD i ^^ (y.getLsbD i ^^ carry i { toFin := ⟨x, x_lt⟩ } y c))

Tactic:
let ⟨y, y_lt⟩ := y

Result:
w i : Nat
i_lt : i < w
x✝ y✝ : BitVec w
c : Bool
x : Nat
x_lt : x < 2 ^ w
y : Nat
y_lt : y < 2 ^ w
⊢ ({ toFin := ⟨x, x_lt⟩ } + { toFin := ⟨y, y_lt⟩ } + setWidth w (ofBool c)).getLsbD i =
    ({ toFin := ⟨x, x_lt⟩ }.getLsbD i ^^
      ({ toFin := ⟨y, y_lt⟩ }.getLsbD i ^^ carry i { toFin := ⟨x, x_lt⟩ } { toFin := ⟨y, y_lt⟩ } c))