simp [Partial.mem_iff]
α : 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}
α : 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