Theorem: Reactor.Hierarchical.obj?_some_nested (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
Tactic:
have ⟨s, hs⟩ := Object.strict_elim $ Object.iff_obj?_some.mpr ho
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
s : StrictMember cpt i' rtr'
hs : StrictMember.object s = o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
s : StrictMember cpt i' rtr'
hs : StrictMember.object s = o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
Tactic:
exact Object.iff_obj?_some.mp $ hs ▸ ⟨.nested h s⟩
State after:
no goals