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
i' : Component.idType cpt
o : Component.type (Component.type α Component.rtr) cpt
h : rtr{Component.rtr}{i} = some rtr'
ho : rtr'[cpt][i'] = some o
⊢ ∃ j, rtr[cpt][j] = some o
Tactic:
cases cpt <;> try cases i'
State after:
case val
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
v✝ : Component.Valued
i' : Component.idType (Component.val v✝)
o : Component.type (Component.type α Component.rtr) (Component.val v✝)
ho : rtr'[Component.val v✝][i'] = some o
⊢ ∃ j, rtr[Component.val v✝][j] = some o

case rtr.none
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
case rtr.none =>
  exists i
  exact Object.iff_obj?_some.mp $ obj?_root_some ho ▸ ⟨.final h⟩
State after:
no goals

State before:
case val
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
v✝ : Component.Valued
i' : Component.idType (Component.val v✝)
o : Component.type (Component.type α Component.rtr) (Component.val v✝)
ho : rtr'[Component.val v✝][i'] = some o
⊢ ∃ j, rtr[Component.val v✝][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
Tactic:
all_goals 
  exact ⟨_, obj?_some_nested h ho⟩
State after:
no goals

State before:
case rtr
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rtr
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][i'] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
cases i'
State after:
case rtr.none
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
exists i
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ rtr[Component.rtr][↑i] = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ rtr[Component.rtr][↑i] = some o
Tactic:
exact Object.iff_obj?_some.mp $ obj?_root_some ho ▸ ⟨.final h⟩
State after:
no goals

State before:
case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
Tactic:
exact ⟨_, obj?_some_nested h ho⟩
State after:
no goals