Theorem: Reactor.Object.strict_elim (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
o : Component.type α cpt
i : ID
m :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i
    | Component.rcn => i
    | Component.val v => i)
    rtr
⊢ ∃ s, StrictMember.object s = Member.object m
Tactic:
cases cpt <;> cases m <;> exists ‹_›
State after:
no goals