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

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ rtr₁{cpt}{i} = none ↔ rtr₂{cpt}{i} = none
Tactic:
simp only [Option.eq_none_iff_forall_not_mem, ←not_exists]
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (¬∃ x, x ∈ rtr₁{cpt}{i}) ↔ ¬∃ x, x ∈ rtr₂{cpt}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (¬∃ x, x ∈ rtr₁{cpt}{i}) ↔ ¬∃ x, x ∈ rtr₂{cpt}{i}
Tactic:
simp [get?_some_iff e]
State after:
no goals