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

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
ho : rtr[Component.rtr][c] = some con
hc : con{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
Tactic:
have ⟨m⟩ := Object.iff_obj?_some.mpr ho
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
m : Member Component.rtr c rtr
ho : rtr[Component.rtr][c] = some (Member.object m)
hc : Member.object m{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
m : Member Component.rtr c rtr
ho : rtr[Component.rtr][c] = some (Member.object m)
hc : Member.object m{cpt}{i} = some 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 $ m.extend_object hc ▸ ⟨m.extend hc⟩
State after:
no goals