Theorem: BVExpr.bitblast.blastSignExtend_empty_eq_zeroExtend (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/SignExtend.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ blastSignExtend aig target = blastZeroExtend aig target
Tactic:
unfold blastSignExtend
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ (match target with
    | { w := width, stream := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, stream := input }
      else { aig := aig, stream := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefStream.empty }) =
    blastZeroExtend aig target

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ (match target with
    | { w := width, stream := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, stream := input }
      else { aig := aig, stream := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefStream.empty }) =
    blastZeroExtend aig target
Tactic:
simp [htarget]
State after:
no goals