-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
    (ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx]'hbounds = aig.decls[idx]

Proof state:
case gate.or
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go aig lhs atomHandler).val.aig.decls.size
this :
  (go aig lhs atomHandler).val.aig.decls.size ≤ (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
hbounds : idx < (go aig (BoolExpr.gate Gate.or lhs rhs) atomHandler).val.aig.decls.size
lih : (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls[idx] = (go aig lhs atomHandler).val.aig.decls[idx]
⊢ (go aig (BoolExpr.gate Gate.or lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [go]

Result:
case gate.or
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
this✝ : aig.decls.size ≤ (go aig lhs atomHandler).val.aig.decls.size
this :
  (go aig lhs atomHandler).val.aig.decls.size ≤ (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
hbounds : idx < (go aig (BoolExpr.gate Gate.or lhs rhs) atomHandler).val.aig.decls.size
lih : (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls[idx] = (go aig lhs atomHandler).val.aig.decls[idx]
⊢ ((go (go aig lhs atomHandler).1.aig rhs atomHandler).1.aig.mkOrCached
            { lhs := (go aig lhs atomHandler).1.ref.cast ⋯,
              rhs := (go (go aig lhs atomHandler).1.aig rhs atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]

Proof state:
case not
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig expr atomHandler).val.aig.decls.size),
    (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig expr.not atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size
⊢ ((go aig expr atomHandler).1.aig.mkNotCached (go aig expr atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]

Tactic:
specialize ih aig (by omega) (by omega)

Result:
case not
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig expr.not atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size
ih : (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ ((go aig expr atomHandler).1.aig.mkNotCached (go aig expr atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]

Proof state:
case const
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.const a✝) atomHandler).val.aig.decls.size
⊢ (go aig (BoolExpr.const a✝) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [go]

Result:
case const
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.const a✝) atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]

Proof state:
case ite
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
discr lhs rhs : BoolExpr α
dih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig discr atomHandler).val.aig.decls.size),
    (go aig discr atomHandler).val.aig.decls[idx] = aig.decls[idx]
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig lhs atomHandler).val.aig.decls.size),
    (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig rhs atomHandler).val.aig.decls.size),
    (go aig rhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (discr.ite lhs rhs) atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go aig discr atomHandler).val.aig.decls.size
⊢ (go aig (discr.ite lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
have := go_le_size atomHandler lhs (go aig discr atomHandler).val.aig

Result:
case ite
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
discr lhs rhs : BoolExpr α
dih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig discr atomHandler).val.aig.decls.size),
    (go aig discr atomHandler).val.aig.decls[idx] = aig.decls[idx]
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig lhs atomHandler).val.aig.decls.size),
    (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig rhs atomHandler).val.aig.decls.size),
    (go aig rhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (discr.ite lhs rhs) atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go aig discr atomHandler).val.aig.decls.size
this :
  (go aig discr atomHandler).val.aig.decls.size ≤
    (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls.size
⊢ (go aig (discr.ite lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Proof state:
case literal
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.literal a✝) atomHandler).val.aig.decls.size
⊢ (go aig (BoolExpr.literal a✝) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [go]

Result:
case literal
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.literal a✝) atomHandler).val.aig.decls.size
⊢ (atomHandler aig a✝).aig.decls[idx] = aig.decls[idx]

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig rhs atomHandler).val.aig.decls.size),
    (go aig rhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.gate g lhs rhs) atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go aig lhs atomHandler).val.aig.decls.size
this :
  (go aig lhs atomHandler).val.aig.decls.size ≤ (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
lih : (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size

Tactic:
omega

Result:
no goals