-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go.eq_def : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache =
    match w, expr with
    | w, Std.Tactic.BVDecide.BVExpr.var a =>
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig { ident := a };
      have this := ⋯;
      have cache := cache.cast this;
      { result := ⟨res, this⟩, cache := cache }
    | w, Std.Tactic.BVDecide.BVExpr.const val =>
      have res := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig val;
      { result := ⟨{ aig := aig, vec := res }, ⋯⟩, cache := cache }
    | w, lhsExpr.bin op rhsExpr =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig lhsExpr cache with
      | { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig_1 rhsExpr cache with
        | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } =>
          let lhs_1 := lhs.cast hraig;
          match op with
          | Std.Tactic.BVDecide.BVBinOp.and =>
            let res := Std.Sat.AIG.RefVec.zip aig_2 { lhs := lhs_1, rhs := rhs } Std.Sat.AIG.mkAndCached;
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.or =>
            let res := Std.Sat.AIG.RefVec.zip aig_2 { lhs := lhs_1, rhs := rhs } Std.Sat.AIG.mkOrCached;
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.xor =>
            let res := Std.Sat.AIG.RefVec.zip aig_2 { lhs := lhs_1, rhs := rhs } Std.Sat.AIG.mkXorCached;
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.add =>
            let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig_2 { lhs := lhs_1, rhs := rhs };
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.mul =>
            let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig_2 { lhs := lhs_1, rhs := rhs };
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.udiv =>
            let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv aig_2 { lhs := lhs_1, rhs := rhs };
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
          | Std.Tactic.BVDecide.BVBinOp.umod =>
            let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod aig_2 { lhs := lhs_1, rhs := rhs };
            have this := ⋯;
            { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, Std.Tactic.BVDecide.BVExpr.un op expr =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache with
      | { result := ⟨{ aig := eaig, vec := evec }, heaig⟩, cache := cache } =>
        match op with
        | Std.Tactic.BVDecide.BVUnOp.not =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastNot eaig evec;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft eaig { vec := evec, distance := distance };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.rotateRight distance =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight eaig { vec := evec, distance := distance };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance =>
          let res :=
            Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst eaig { vec := evec, distance := distance };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.reverse =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse eaig evec;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.clz =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastClz eaig evec;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
        | Std.Tactic.BVDecide.BVUnOp.cpop =>
          let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop eaig evec;
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, lhs.append rhs h =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig lhs cache with
      | { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig_1 rhs cache with
        | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } =>
          have lhs_1 := lhs.cast hraig;
          let res :=
            Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig_2
              { lw := l, rw := r, lhs := lhs_1, rhs := rhs, h := ⋯ };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache with
      | { result := ⟨{ aig := aig_1, vec := expr }, haig⟩, cache := cache } =>
        let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate aig_1 { w := w_1, n := n, inner := expr, h := h };
        have this := ⋯;
        { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache with
      | { result := ⟨{ aig := eaig, vec := evec }, heaig⟩, cache := cache } =>
        let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract eaig { w := w, vec := evec, start := start };
        have this := ⋯;
        { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, lhs.shiftLeft rhs =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig lhs cache with
      | { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig_1 rhs cache with
        | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } =>
          let lhs_1 := lhs.cast hraig;
          let res :=
            Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft aig_2 { n := n, target := lhs_1, distance := rhs };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, lhs.shiftRight rhs =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig lhs cache with
      | { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig_1 rhs cache with
        | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } =>
          let lhs_1 := lhs.cast hraig;
          let res :=
            Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight aig_2 { n := n, target := lhs_1, distance := rhs };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }
    | w, lhs.arithShiftRight rhs =>
      match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig lhs cache with
      | { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig_1 rhs cache with
        | { result := ⟨{ aig := aig_2, vec := rhs }, hraig⟩, cache := cache } =>
          let lhs_1 := lhs.cast hraig;
          let res :=
            Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight aig_2 { n := n, target := lhs_1, distance := rhs };
          have this := ⋯;
          { result := ⟨res, this⟩, cache := cache.cast ⋯ }