internlm/Lean-Github huggingface dataset:
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 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]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
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.decls[idx] = aig.decls[idx]

case gate.or.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.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]
⊢ 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.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.decls[idx] = aig.decls[idx]

case gate.or.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.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]
⊢ 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.xor
α β : 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.xor 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.xor lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case gate.xor
α β : 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.xor 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.mkXorCached
            { 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.xor
α β : 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.xor 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.mkXorCached
            { 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 := mkXorCached)]
Proof state after:
case gate.xor
α β : 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.xor 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.xor.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.xor 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.xor
α β : 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.xor 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.xor.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.xor 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.beq
α β : 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.beq 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.beq lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case gate.beq
α β : 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.beq 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.mkBEqCached
            { 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.beq
α β : 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.beq 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.mkBEqCached
            { 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 := mkBEqCached)]
Proof state after:
case gate.beq
α β : 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.beq 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.beq.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.beq 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.beq
α β : 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.beq 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.beq.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.beq 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.imp
α β : 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.imp 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.imp lhs rhs) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case gate.imp
α β : 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.imp 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.mkImpCached
            { 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.imp
α β : 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.imp 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.mkImpCached
            { 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 := mkImpCached)]
Proof state after:
case gate.imp
α β : 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.imp 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.imp.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.imp 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.imp
α β : 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.imp 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.imp.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.imp 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_IsPrefix_aig
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ IsPrefix aig.decls (go expr aig atomHandler).val.aig.decls
Tactic:
apply IsPrefix.of
Proof state after:
case idx_eq
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]

case size_le
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size