-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig)
    (assign : α → Bool) :
    ⟦blastGetLsbD aig target, assign⟧
      =
    if h : target.idx < target.w then
      ⟦aig, target.vec.get target.idx h, assign⟧
    else
      false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign,
      if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }
      else aig.mkConstCached false⟧ =
    if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
      ⟦assign, { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }⟧
    else false

Tactic:
dsimp only

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign, if h : idx < w✝ then { aig := aig, ref := expr.get idx h } else aig.mkConstCached false⟧ =
    if h : idx < w✝ then ⟦assign, { aig := aig, ref := expr.get idx h }⟧ else false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign, if h : idx < w✝ then { aig := aig, ref := expr.get idx h } else aig.mkConstCached false⟧ =
    if h : idx < w✝ then ⟦assign, { aig := aig, ref := expr.get idx h }⟧ else false

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
target : GetLsbDTarget aig
assign : α → Bool
⊢ ⟦assign, blastGetLsbD aig target⟧ =
    if h : target.idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get target.idx h }⟧ else false

Tactic:
rcases target with ⟨expr, idx⟩

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign, blastGetLsbD aig (GetLsbDTarget.mk expr idx)⟧ =
    if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
      ⟦assign, { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }⟧
    else false

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign, blastGetLsbD aig (GetLsbDTarget.mk expr idx)⟧ =
    if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
      ⟦assign, { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }⟧
    else false

Tactic:
unfold blastGetLsbD

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefVec w✝
idx : Nat
⊢ ⟦assign,
      if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }
      else aig.mkConstCached false⟧ =
    if h : (GetLsbDTarget.mk expr idx).idx < (GetLsbDTarget.mk expr idx).w then
      ⟦assign, { aig := aig, ref := (GetLsbDTarget.mk expr idx).vec.get (GetLsbDTarget.mk expr idx).idx h }⟧
    else false