Theorem: Dependency.Acyclic.of_trivial (ReactorModel/Execution/Theorems/Dependency.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ Acyclic rtr
Tactic:
simp_all [Dependency.Acyclic.iff_mem_acyclic, triv]
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ ∀ i ∈ ∅, ¬i <[rtr] i

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ ∀ i ∈ ∅, ¬i <[rtr] i
Tactic:
intros _ h
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
i✝ : Component.idType Component.rcn
h : i✝ ∈ ∅
⊢ ¬i✝ <[rtr] i✝

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
i✝ : Component.idType Component.rcn
h : i✝ ∈ ∅
⊢ ¬i✝ <[rtr] i✝
Tactic:
exact absurd h Partial.not_mem_empty
State after:
no goals