-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
theorem denote_getD_eq_getLsbD (aig : AIG α) (assign : α → Bool) (x : BitVec w)
    (xv : AIG.RefVec aig w) (falseRef : AIG.Ref aig)
    (hx : ∀ idx hidx, ⟦aig, xv.get idx hidx, assign⟧ = x.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false) :
    ∀ idx, ⟦aig, xv.getD idx falseRef, assign⟧ = x.getLsbD idx

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : idx < w
⊢ ⟦assign, { aig := aig, ref := xv.get idx h✝ }⟧ = x.getLsbD idx

Tactic:
rw [hx]

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ ⟦assign, { aig := aig, ref := falseRef }⟧ = x.getLsbD idx

Tactic:
rw [hfalse]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ false = x.getLsbD idx

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ x.getLsbD idx = false

Tactic:
apply BitVec.getLsbD_ge

Result:
case isFalse.ge
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ w ≤ idx

Proof state:
case isFalse.ge
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ w ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
⊢ ⟦assign, { aig := aig, ref := if hidx : idx < w then xv.get idx hidx else falseRef }⟧ = x.getLsbD idx

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : idx < w
⊢ ⟦assign, { aig := aig, ref := xv.get idx h✝ }⟧ = x.getLsbD idx

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ ⟦assign, { aig := aig, ref := falseRef }⟧ = x.getLsbD idx

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ false = x.getLsbD idx

Tactic:
symm

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
h✝ : ¬idx < w
⊢ x.getLsbD idx = false

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
⊢ ⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx

Tactic:
rw [AIG.RefVec.getD]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
⊢ ⟦assign, { aig := aig, ref := if hidx : idx < w then xv.get idx hidx else falseRef }⟧ = x.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
⊢ ∀ (idx : Nat), ⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx

Tactic:
intro idx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
x : BitVec w
xv : aig.RefVec w
falseRef : aig.Ref
hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
idx : Nat
⊢ ⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx