-- 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:
α : 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
⊢ 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

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
a : α
h : aig.decls[start] = Decl.atom a
⊢ aig.decls[start] = Decl.atom ?a

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
a : α
h : aig.decls[start] = Decl.atom a
⊢ α

Tactic:
assumption

Result:
no goals

Proof state:
α : 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
⊢ prop

Tactic:
apply hgate

Result:
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

Proof state:
α : 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
⊢ prop

Tactic:
apply hconst

Result:
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

Proof state:
α : 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
a : α
h : aig.decls[start] = Decl.atom a
⊢ prop

Tactic:
apply hatom

Result:
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
a : α
h : aig.decls[start] = Decl.atom a
⊢ aig.decls[start] = Decl.atom ?a

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
a : α
h : aig.decls[start] = Decl.atom a
⊢ α