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

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    none
⊢ rtr{cpt}{i} = none
Tactic:
replace ho := Object.not_iff_obj?_none.mpr ho
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
⊢ rtr{cpt}{i} = none

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
⊢ rtr{cpt}{i} = none
Tactic:
by_contra h
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
h : ¬rtr{cpt}{i} = none
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
h : ¬rtr{cpt}{i} = none
⊢ False
Tactic:
exact ho _ ⟨.final $ Option.ne_none_iff_exists.mp h |>.choose_spec.symm⟩
State after:
no goals