-- 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.beq
α β : 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.beq 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.beq lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [go]

Result:
case gate.beq
α β : 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.beq 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.mkBEqCached
            { 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:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
discr 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 (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
this :
  (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls.size ≤
    (go (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
dih : (go aig discr atomHandler).val.aig.decls[idx] = aig.decls[idx]
lih :
  (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls[idx] =
    (go aig discr atomHandler).val.aig.decls[idx]
⊢ idx < (go (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size

Tactic:
omega

Result:
no goals

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
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]

Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]

Result:
no goals

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
idx : Nat
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]

Tactic:
induction expr generalizing aig with
| const =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
| literal =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
| not expr ih =>
  simp only [go]
  have := go_le_size atomHandler expr aig
  specialize ih aig (by omega) (by omega)
  rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
  assumption
| ite discr lhs rhs dih lih rih =>
  have := go_le_size atomHandler discr aig
  have := go_le_size atomHandler lhs (go aig discr atomHandler).val.aig
  have := go_le_size atomHandler rhs (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig
  specialize dih aig (by omega) (by omega)
  specialize lih (go aig discr atomHandler).val.aig (by omega) (by omega)
  specialize rih (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig (by omega) (by omega)
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih]
| gate g lhs rhs lih rih =>
  have := go_le_size atomHandler lhs aig
  have := go_le_size atomHandler rhs (go aig lhs atomHandler).val.aig
  specialize lih aig (by omega) (by omega)
  specialize rih (go aig lhs atomHandler).val.aig (by omega) (by omega)
  cases g with
  | and =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkAndCached), rih, lih]
  | xor =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkXorCached), rih, lih]
  | beq =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
  | or =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]

Result:
no goals