-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) :
    carry (i+1) x (1#w) false = decide (∀ j ≤ i, x.getLsbD j = true)

Proof state:
case succ.false
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
⊢ (false && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

case succ.true
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (true && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
case false =>
  have : ∃ j ≤ i + 1, x.getLsbD j = false :=
    ⟨i+1, by omega, hx⟩
  simpa

Result:
case succ.true
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (true && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Proof state:
case mpr
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true) → ∀ (j : Nat), j ≤ i → x.getLsbD j = true

Tactic:
intro h j hj

Result:
case mpr
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true
j : Nat
hj : j ≤ i
⊢ x.getLsbD j = true

Proof state:
case zero
w : Nat
x : BitVec w
h : 0 < w
⊢ carry (0 + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ 0 → x.getLsbD j = true)

Tactic:
simp [carry_succ, h]

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
⊢ x.getLsbD j = true

Tactic:
rcases Nat.le_or_eq_of_le_succ hj with (hj' | rfl)

Result:
case mp.inl
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
hj' : j ≤ i
⊢ x.getLsbD j = true

case mp.inr
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
hj : i.succ ≤ i + 1
⊢ x.getLsbD i.succ = true

Proof state:
case mp.inl.a
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
hj' : j ≤ i
⊢ j ≤ i

Tactic:
assumption

Result:
no goals

Proof state:
case mpr.a
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true
j : Nat
hj : j ≤ i
⊢ j ≤ i + 1

Tactic:
omega

Result:
no goals