-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
    getMsbD (setWidth' ge x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m))

Proof state:
case neg
m n : Nat
x : BitVec n
i : Nat
ge : n ≤ m
h₁ : i < m
h₂ : i < m - n
h₃ : n ≤ i + n - m
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ x.getLsbD (m - 1 - i) = false

Tactic:
apply getLsbD_ge

Result:
case neg.ge
m n : Nat
x : BitVec n
i : Nat
ge : n ≤ m
h₁ : i < m
h₂ : i < m - n
h₃ : n ≤ i + n - m
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ n ≤ m - 1 - i

Proof state:
case neg
m n : Nat
x : BitVec n
i : Nat
ge : n ≤ m
h₁ : i < m
h₂ : i < m - n
h₃ : n ≤ i + n - m
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ x.getLsbD (m - 1 - i) = false

Tactic:
try apply getLsbD_ge

Result:
case neg.ge
m n : Nat
x : BitVec n
i : Nat
ge : n ≤ m
h₁ : i < m
h₂ : i < m - n
h₃ : n ≤ i + n - m
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ n ≤ m - 1 - i

Proof state:
case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case pos
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

case neg
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
h₁ : ¬decide (i < m) = true
h₂ : ¬decide (m - n ≤ i) = true
h₃ : ¬decide (i + n - m < n) = true
h₄ : ¬n - 1 - (i + n - m) = m - 1 - i
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

Tactic:
all_goals
  simp only [h₁, h₂, h₃, h₄]
  simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
    Bool.false_and, Bool.and_self] <;>
  (try apply getLsbD_ge) <;>
  (try apply (getLsbD_ge _ _ _).symm) <;>
  omega

Result:
no goals