internlm/Lean-Github huggingface dataset:
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case not
α β : Type
inst✝³ : BEq β
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 expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go expr aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case not.h1
α β : Type
inst✝³ : BEq β
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 expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go expr aig atomHandler).1.aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
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 expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ idx < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
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 expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ idx < (go expr aig atomHandler).val.aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler lhs aig
Proof state after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
Proof state after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
specialize lih aig (by omega) (by omega)
Proof state after:
case gate
α β : Type
inst✝³ : BEq β
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 rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate
α β : Type
inst✝³ : BEq β
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 rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
specialize rih (go lhs aig atomHandler).val.aig (by omega) (by omega)
Proof state after:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
cases g with
| and =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
  rw [rih, lih]
| or =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
  rw [rih, lih]
| xor =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
  rw [rih, lih]
| beq =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
  rw [rih, lih]
| imp =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
  rw [rih, lih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ idx < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
lih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go lhs aig atomHandler).val.aig.decls.size),
    (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
⊢ idx < (go lhs aig atomHandler).val.aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
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 rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go lhs aig atomHandler).val.aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
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 rhs aig atomHandler).val.aig.decls.size),
    (go rhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.gate g lhs rhs) aig atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate.and
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case gate.and
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkAndCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate.and
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkAndCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
Proof state after:
case gate.and
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.and.h1
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate.and
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case gate.and.h1
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.and lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ idx < (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.decls.size
Tactic:
rw [rih, lih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case gate.or
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case gate.or
α β : Type
inst✝³ : BEq β
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 lhs aig atomHandler).val.aig.decls.size
this :
  (go lhs aig atomHandler).val.aig.decls.size ≤ (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls.size
hbounds : idx < (go (BoolExpr.gate Gate.or lhs rhs) aig atomHandler).val.aig.decls.size
lih : (go lhs aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go rhs (go lhs aig atomHandler).val.aig atomHandler).val.aig.decls[idx] = (go lhs aig atomHandler).val.aig.decls[idx]
⊢ ((go rhs (go lhs aig atomHandler).1.aig atomHandler).1.aig.mkOrCached
            { lhs := (go lhs aig atomHandler).1.ref.cast ⋯,
              rhs := (go rhs (go lhs aig atomHandler).1.aig atomHandler).1.ref }).aig.decls[idx] =
    aig.decls[idx]