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

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 hconst
Proof state after:
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