-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_reverse {i : Nat} {x : BitVec w} :
    (x.reverse).getLsbD i = x.getMsbD i

Proof state:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (decide (n - (n + 1) ≤ i) && x.getMsbD (i + (n + 1) - n)) = x.getMsbD (i + 1)

Tactic:
simp only [show n - (n + 1) = 0 by omega, Nat.zero_le, decide_true, Bool.true_and]

Result:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ x.getMsbD (i + (n + 1) - n) = x.getMsbD (i + 1)

Proof state:
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n + 1)
⊢ (if i = 0 then x.msb else (setWidth n x).reverse.getLsbD (i - 1)) = x.getMsbD i

Tactic:
rcases i with rfl | i

Result:
case zero
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
⊢ (if 0 = 0 then x.msb else (setWidth n x).reverse.getLsbD (0 - 1)) = x.getMsbD 0

case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (if i + 1 = 0 then x.msb else (setWidth n x).reverse.getLsbD (i + 1 - 1)) = x.getMsbD (i + 1)

Proof state:
w i : Nat
x : BitVec w
⊢ x.reverse.getLsbD i = x.getMsbD i

Tactic:
induction w generalizing i

Result:
case zero
i : Nat
x : BitVec 0
⊢ x.reverse.getLsbD i = x.getMsbD i

case succ
n✝ : Nat
a✝ : ∀ {i : Nat} {x : BitVec n✝}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n✝ + 1)
⊢ x.reverse.getLsbD i = x.getMsbD i

Proof state:
case zero
i : Nat
x : BitVec 0
⊢ x.reverse.getLsbD i = x.getMsbD i

case succ
n✝ : Nat
a✝ : ∀ {i : Nat} {x : BitVec n✝}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n✝ + 1)
⊢ x.reverse.getLsbD i = x.getMsbD i

Tactic:
case zero => simp

Result:
case succ
n✝ : Nat
a✝ : ∀ {i : Nat} {x : BitVec n✝}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n✝ + 1)
⊢ x.reverse.getLsbD i = x.getMsbD i

Proof state:
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n + 1)
⊢ x.reverse.getLsbD i = x.getMsbD i

Tactic:
simp only [reverse, truncate_eq_setWidth, getLsbD_concat]

Result:
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
i : Nat
x : BitVec (n + 1)
⊢ (if i = 0 then x.msb else (setWidth n x).reverse.getLsbD (i - 1)) = x.getMsbD i

Proof state:
case zero
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
⊢ (if 0 = 0 then x.msb else (setWidth n x).reverse.getLsbD (0 - 1)) = x.getMsbD 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (setWidth n x).getMsbD i = x.getMsbD (i + 1)

Tactic:
rw [getMsbD_setWidth]

Result:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (decide (n - (n + 1) ≤ i) && x.getMsbD (i + (n + 1) - n)) = x.getMsbD (i + 1)

Proof state:
case succ.e_i
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ i + (n + 1) - n = i + 1

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ n - (n + 1) = 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (if i + 1 = 0 then x.msb else (setWidth n x).reverse.getLsbD (i + 1 - 1)) = x.getMsbD (i + 1)

Tactic:
simp only [Nat.add_one_ne_zero, ↓reduceIte, Nat.add_one_sub_one, ih]

Result:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ (setWidth n x).getMsbD i = x.getMsbD (i + 1)

Proof state:
i : Nat
x : BitVec 0
⊢ x.reverse.getLsbD i = x.getMsbD i

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ x.getMsbD (i + (n + 1) - n) = x.getMsbD (i + 1)

Tactic:
congr

Result:
case succ.e_i
n : Nat
ih : ∀ {i : Nat} {x : BitVec n}, x.reverse.getLsbD i = x.getMsbD i
x : BitVec (n + 1)
i : Nat
⊢ i + (n + 1) - n = i + 1