Theorem: Reactor.equiv_eq_dependencies (ReactorModel/Execution/Theorems/Reactor.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
⊢ dependencies rtr₁ = dependencies rtr₂
Tactic:
ext i j
State after:
case h.h
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
i j : ID
⊢ j ∈ dependencies rtr₁ i ↔ j ∈ dependencies rtr₂ i

State before:
case h.h
α : Type
inst✝ : Hierarchical α
rtr₂ rtr₁ : α
e : rtr₁ ≈ rtr₂
i j : ID
⊢ j ∈ dependencies rtr₁ i ↔ j ∈ dependencies rtr₂ i
Tactic:
exact ⟨.equiv $ .symm e, .equiv e⟩
State after:
no goals