Theorem: Reactor.Equivalent.ids_eq (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
⊢ Partial.ids (rtr₁[cpt]) = Partial.ids (rtr₂[cpt])
Tactic:
ext1
State after:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
x✝ : Component.idType cpt
⊢ x✝ ∈ Partial.ids (rtr₁[cpt]) ↔ x✝ ∈ Partial.ids (rtr₂[cpt])

State before:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
x✝ : Component.idType cpt
⊢ x✝ ∈ Partial.ids (rtr₁[cpt]) ↔ x✝ ∈ Partial.ids (rtr₂[cpt])
Tactic:
exact mem_iff e
State after:
no goals