-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size}
    (hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
    (hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
    (hgate :
      ∀ lhs rhs linv rinv,
        aig.decls[start]'hstart = .gate lhs rhs linv rinv
          →
        ⟦aig, ⟨start, hstart⟩, assign⟧ = res
    ) :
    ⟦aig, ⟨start, hstart⟩, assign⟧ = res

Proof state:
case hconst
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

Tactic:
exact hconst

Result:
no goals

Proof state:
case hgate
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

Tactic:
exact hgate

Result:
no goals

Proof state:
case hatom
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

Tactic:
exact hatom

Result:
no goals

Proof state:
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

Tactic:
apply idx_trichotomy aig hstart

Result:
case hconst
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

case hatom
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res

case hgate
α : Type
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 → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = res