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

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
have ⟨s, hs⟩ := Object.strict_elim $ Object.iff_obj?_some.mpr ho
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
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
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
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
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
have ⟨c, ⟨m, hm⟩⟩ := s.split'
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
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
c : WithTop ID
m : Member Component.rtr c rtr
hm : Member.object m{cpt}{i} = some (StrictMember.object s)
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
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
c : WithTop ID
m : Member Component.rtr c rtr
hm : Member.object m{cpt}{i} = some (StrictMember.object s)
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
exact ⟨c, m.object, Object.iff_obj?_some.mp ⟨m⟩, hs ▸ hm⟩
State after:
no goals