Theorem: Reactor.RootEqualUpTo.mem_iff (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
c : Component
j : ID
e : rtr₁ ≃[cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ j ∈ rtr₁{c} ↔ j ∈ rtr₂{c}
Tactic:
simp [Partial.mem_iff]
State after:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
c : Component
j : ID
e : rtr₁ ≃[cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ (∃ b, rtr₁{c}{j} = some b) ↔ ∃ b, rtr₂{c}{j} = some b