-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} :
    (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b

Proof state:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
a✝ : i < w + 1
⊢ b = false

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : i < w
⊢ i < w + 1

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
b : Bool
x : BitVec w
⊢ (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b

Tactic:
simp only [getMsbD_eq_getLsbD, Nat.add_sub_cancel, getLsbD_concat]

Result:
i w : Nat
b : Bool
x : BitVec w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Proof state:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
⊢ i < w + 1 → b = false

Tactic:
intro

Result:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
a✝ : i < w + 1
⊢ b = false

Proof state:
i w : Nat
b : Bool
x : BitVec w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Tactic:
by_cases h₀ : i = w

Result:
case pos
i w : Nat
b : Bool
x : BitVec w
h₀ : i = w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Proof state:
case pos
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : i < w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Tactic:
simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm]

Result:
no goals

Proof state:
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
⊢ w - i = 0

Tactic:
omega

Result:
no goals

Proof state:
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : i < w
⊢ ¬w - i = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Tactic:
by_cases h₁ : i < w

Result:
case pos
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : i < w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Proof state:
case pos
i w : Nat
b : Bool
x : BitVec w
h₀ : i = w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Tactic:
simp [h₀]

Result:
no goals

Proof state:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
⊢ (decide (i < w + 1) && if w - i = 0 then b else x.getLsbD (w - i - 1)) =
    if i < w then decide (i < w) && x.getLsbD (w - 1 - i) else decide (i = w) && b

Tactic:
simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_false, Bool.false_and,
  Bool.and_eq_false_imp, decide_eq_true_eq]

Result:
case neg
i w : Nat
b : Bool
x : BitVec w
h₀ : ¬i = w
h₁ : ¬i < w
⊢ i < w + 1 → b = false