-- 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
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:
simp only [h₁, h₂, h₃, h₄]

Result:
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
⊢ (false && x.getLsbD (m - 1 - i)) = (false && (false && x.getLsbD (n - 1 - (i + n - m))))

Proof state:
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
⊢ (false && x.getLsbD (m - 1 - i)) = (false && (false && x.getLsbD (n - 1 - (i + n - m))))

Tactic:
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

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

Tactic:
apply (getLsbD_ge _ _ _).symm

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

Proof state:
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
⊢ (setWidth' ge x).getMsbD i = (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Tactic:
simp only [getMsbD, getLsbD_setWidth', gt_iff_lt]

Result:
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
⊢ (decide (i < m) && x.getLsbD (m - 1 - i)) =
    (decide (m - n ≤ i) && (decide (i + n - m < n) && x.getLsbD (n - 1 - (i + n - m))))

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

Tactic:
try apply (getLsbD_ge _ _ _).symm

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

Proof state:
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
⊢ (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:
by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (m - n ≤ i) <;> by_cases h₃ : decide (i + n - m < n) <;>
  by_cases h₄ : n - 1 - (i + n - m) = m - 1 - i

Result:
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))))