-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
    x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n

Proof state:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

Tactic:
simp only [h₂, ↓reduceIte]

Result:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

Proof state:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

Tactic:
by_cases h₂ : n + ↑i < w

Result:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

Proof state:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

Tactic:
by_cases h₃ : m + (n + ↑i) < w

Result:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : m + (n + i) < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : ¬m + (n + i) < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

Proof state:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

Tactic:
simp only [h₁, decide_false, Bool.not_false, Bool.true_and]

Result:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

Proof state:
case pred
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

Tactic:
by_cases h₁ : w ≤ (i : Nat)

Result:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : w ≤ i
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

Proof state:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : n + i < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
    else (x.sshiftRight m).msb

Tactic:
simp [h₂]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
m n : Nat
⊢ x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
⊢ (x.sshiftRight (m + n)).getLsbD i = ((x.sshiftRight m).sshiftRight n).getLsbD i

Proof state:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : m + (n + i) < w
⊢ x.getLsbD (m + (n + i)) = x.msb

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
⊢ (x.sshiftRight (m + n)).getLsbD i = ((x.sshiftRight m).sshiftRight n).getLsbD i

Tactic:
simp only [getLsbD_sshiftRight, Nat.add_assoc]

Result:
case pred
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

Proof state:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : m + (n + i) < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

Tactic:
simp [h₃]

Result:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : m + (n + i) < w
⊢ x.getLsbD (m + (n + i)) = x.msb

Proof state:
case pos
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : w ≤ i
⊢ (!decide (w ≤ i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) =
    (!decide (w ≤ i) &&
      if n + i < w then !decide (w ≤ n + i) && if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb
      else (x.sshiftRight m).msb)

Tactic:
simp [h₁]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
m n i : Nat
a✝ : i < w
h₁ : ¬w ≤ i
h₂ : ¬n + i < w
h₃ : ¬m + (n + i) < w
⊢ (if m + (n + i) < w then x.getLsbD (m + (n + i)) else x.msb) = (x.sshiftRight m).msb

Tactic:
simp [h₃, msb_sshiftRight]

Result:
no goals