-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_of_getMsbD_eq {x y : BitVec w}
    (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ w - 1 - i < w

Tactic:
simp only [Nat.sub_sub]

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ w - (1 + i) < w

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ x.getLsbD i = y.getLsbD i

Tactic:
have q_lt : w - 1 - i < w := by
  simp only [Nat.sub_sub]
  apply Nat.sub_lt w_pos
  simp [Nat.succ_add]

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
q_lt : w - 1 - i < w
⊢ x.getLsbD i = y.getLsbD i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ 0 < 1 + i

Tactic:
simp [Nat.succ_add]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
q_lt : w - 1 - i < w
⊢ x.getLsbD i = y.getLsbD i

Tactic:
have q := pred (w - 1 - i) q_lt

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
q_lt : w - 1 - i < w
q :
  (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i))) =
    (decide (w - 1 - i < w) && y.getLsbD (w - 1 - (w - 1 - i)))
⊢ x.getLsbD i = y.getLsbD i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
⊢ i + 1 ≤ w

Tactic:
exact i_lt

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
q_lt : w - 1 - i < w
q :
  (decide (w - 1 - i < w) && x.getLsbD (w - 1 - (w - 1 - i))) =
    (decide (w - 1 - i < w) && y.getLsbD (w - 1 - (w - 1 - i)))
⊢ x.getLsbD i = y.getLsbD i

Tactic:
simpa [q_lt, Nat.sub_sub_self, r] using q

Result:
no goals

Proof state:
case pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
⊢ x.getLsbD i = y.getLsbD i

Tactic:
if w_zero : w = 0 then
  simp [w_zero]
else
  have w_pos := Nat.pos_of_ne_zero w_zero
  have r : i ≤ w - 1 := by
    simp [Nat.le_sub_iff_add_le w_pos]
    exact i_lt
  have q_lt : w - 1 - i < w := by
    simp only [Nat.sub_sub]
    apply Nat.sub_lt w_pos
    simp [Nat.succ_add]
  have q := pred (w - 1 - i) q_lt
  simpa [q_lt, Nat.sub_sub_self, r] using q

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
⊢ x = y

Tactic:
apply eq_of_getLsbD_eq

Result:
case pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
⊢ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
⊢ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i

Tactic:
intro i i_lt

Result:
case pred
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
⊢ x.getLsbD i = y.getLsbD i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : w = 0
⊢ x.getLsbD i = y.getLsbD i

Tactic:
simp [w_zero]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → x.getMsbD i = y.getMsbD i
⊢ x = y

Tactic:
simp only [getMsbD] at pred

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
⊢ x = y

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
⊢ x.getLsbD i = y.getLsbD i

Tactic:
have r : i ≤ w - 1 := by
  simp [Nat.le_sub_iff_add_le w_pos]
  exact i_lt

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ x.getLsbD i = y.getLsbD i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ w - (1 + i) < w

Tactic:
apply Nat.sub_lt w_pos

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
r : i ≤ w - 1
⊢ 0 < 1 + i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
⊢ x.getLsbD i = y.getLsbD i

Tactic:
have w_pos := Nat.pos_of_ne_zero w_zero

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
⊢ x.getLsbD i = y.getLsbD i

Proof state:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
⊢ i ≤ w - 1

Tactic:
simp [Nat.le_sub_iff_add_le w_pos]

Result:
w : Nat
x y : BitVec w
pred : ∀ (i : Nat), i < w → (decide (i < w) && x.getLsbD (w - 1 - i)) = (decide (i < w) && y.getLsbD (w - 1 - i))
i : Nat
i_lt : i < w
w_zero : ¬w = 0
w_pos : 0 < w
⊢ i + 1 ≤ w