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

Proof state:
case a
α : Type
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✝¹ : 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✝¹ : 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✝¹ : 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✝¹ : 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

Result:
no goals

Proof state:
case a
α : Type
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✝¹ : 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

Result:
no goals