-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
    (h : x &&& y = 0#w) : x + y = x ||| y

Proof state:
case step.right
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Tactic:
by_cases hx : x.getLsbD i <;> simp_all [hx]

Result:
no goals

Proof state:
case step.left
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
hx : x.getLsbD ↑i = true
⊢ y.getLsbD ↑i = false

Tactic:
simp_all [hx]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ x + y = x ||| y

Tactic:
rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (x ||| y)]

Result:
case init
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ false = false

case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ∀ (i : Fin w), adcb (x.getLsbD ↑i) (y.getLsbD ↑i) false = (false, (x ||| y).getLsbD ↑i)

Proof state:
case step.left
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ x.getLsbD ↑i = true → y.getLsbD ↑i = false

Tactic:
intros hx

Result:
case step.left
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
hx : x.getLsbD ↑i = true
⊢ y.getLsbD ↑i = false

Proof state:
case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ∀ (i : Fin w),
    (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Tactic:
intros i

Result:
case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
i : Fin w
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Proof state:
case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ∀ (i : Fin w), adcb (x.getLsbD ↑i) (y.getLsbD ↑i) false = (false, (x ||| y).getLsbD ↑i)

Tactic:
simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsbD_or,
Prod.mk.injEq, and_eq_false_imp]

Result:
case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ ∀ (i : Fin w),
    (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Proof state:
case step
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Tactic:
constructor

Result:
case step.left
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ x.getLsbD ↑i = true → y.getLsbD ↑i = false

case step.right
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Proof state:
case step
w : Nat
x y : BitVec w
i : Fin w
h : (x &&& y).getLsbD ↑i = (0#w).getLsbD ↑i
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Tactic:
simp only [getLsbD_and, getLsbD_zero, and_eq_false_imp] at h

Result:
case step
w : Nat
x y : BitVec w
i : Fin w
h : x.getLsbD ↑i = true → y.getLsbD ↑i = false
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Proof state:
case step
w : Nat
x y : BitVec w
h : x &&& y = 0#w
i : Fin w
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Tactic:
replace h : (x &&& y).getLsbD i = (0#w).getLsbD i := by rw [h]

Result:
case step
w : Nat
x y : BitVec w
i : Fin w
h : (x &&& y).getLsbD ↑i = (0#w).getLsbD ↑i
⊢ (x.getLsbD ↑i = true → y.getLsbD ↑i = false) ∧ (x.getLsbD ↑i ^^ y.getLsbD ↑i) = (x.getLsbD ↑i || y.getLsbD ↑i)

Proof state:
case init
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ false = false

Tactic:
rfl

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x &&& y = 0#w
i : Fin w
⊢ (x &&& y).getLsbD ↑i = (0#w).getLsbD ↑i

Tactic:
rw [h]

Result:
no goals