Theorem: Reactor.Equivalent.get?_some_iff (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (∃ o, rtr₁{cpt}{i} = some o) ↔ ∃ o, rtr₂{cpt}{i} = some o
Tactic:
simp [←Partial.mem_iff, mem_get?_iff e]
State after:
no goals