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

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ Acyclic rtr ↔ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
apply not_iff_not.mp
State after:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ ¬Acyclic rtr ↔ ¬∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ ¬Acyclic rtr ↔ ¬∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
simp [Acyclic]
State after:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ (∃ x, x <[rtr] x) ↔ ∃ x ∈ rtr[Component.rcn], x <[rtr] x

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ (∃ x, x <[rtr] x) ↔ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
constructor <;> intro ⟨d, h⟩
State after:
case mp
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x

case mpr
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
case mp  => exact ⟨_, h.mem₁, h⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x
Tactic:
case mpr => exact ⟨_, h.right⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : ID
h : d <[rtr] d
⊢ ∃ x ∈ rtr[Component.rcn], x <[rtr] x
Tactic:
exact ⟨_, h.mem₁, h⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
d : Component.idType Component.rcn
h : d ∈ rtr[Component.rcn] ∧ d <[rtr] d
⊢ ∃ x, x <[rtr] x
Tactic:
exact ⟨_, h.right⟩
State after:
no goals