internlm/Lean-Github huggingface dataset:
Theorem: AIG.denote_idx_gate
Proof state before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
next heq =>
rw [h] at heq
simp_all
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
rw [h] at heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.gate lhs rhs linv rinv = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.gate lhs rhs linv rinv = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
simp_all
Proof state after:
no goals
Theorem: AIG.idx_trichotomy
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
⊢ prop
Tactic:
match h:aig.decls[start]'hstart with
| .const b => apply hconst; assumption
| .atom a => apply hatom; assumption
| .gate lhs rhs linv rinv => apply hgate; assumption
Proof state after:
no goals
Theorem: AIG.idx_trichotomy
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ prop
Tactic:
apply hconst
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ aig.decls[start] = Decl.const ?b

case b
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ Bool
Theorem: AIG.idx_trichotomy
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ aig.decls[start] = Decl.const ?b

case b
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ Bool
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.idx_trichotomy
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ prop
Tactic:
apply hatom
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ aig.decls[start] = Decl.atom ?a

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ α
Theorem: AIG.idx_trichotomy
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ aig.decls[start] = Decl.atom ?a

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ α
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.idx_trichotomy
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ prop
Tactic:
apply hgate
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ aig.decls[start] = Decl.gate ?lhs ?rhs ?linv ?rinv

case lhs
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Nat

case rhs
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Nat

case linv
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Bool

case rinv
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Bool
Theorem: AIG.idx_trichotomy
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ aig.decls[start] = Decl.gate ?lhs ?rhs ?linv ?rinv

case lhs
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Nat

case rhs
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Nat

case linv
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Bool

case rinv
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Bool
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.denote_idx_trichotomy
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
apply idx_trichotomy aig hstart
Proof state after:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Theorem: AIG.denote_idx_trichotomy
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
. exact hatom
Proof state after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Theorem: AIG.denote_idx_trichotomy
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
. exact hgate
Proof state after:
no goals
Theorem: AIG.denote_idx_trichotomy
Proof state before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hconst
Proof state after:
no goals
Theorem: AIG.denote_idx_trichotomy
Proof state before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hatom
Proof state after:
no goals
Theorem: AIG.denote_idx_trichotomy
Proof state before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hgate
Proof state after:
no goals