Theorem: Reactor.LawfulMemUpdate.obj?_some₁ (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ ∃ o, rtr₁[Component.val cpt][i] = some o
Tactic:
induction u
State after:
case final
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o

case nested
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
case final           => exact ⟨_, get?_some_to_obj?_some ‹_›⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
case nested h _ _ hi => exact ⟨_, obj?_some_nested h hi.choose_spec⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, get?_some_to_obj?_some ‹_›⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, obj?_some_nested h hi.choose_spec⟩
State after:
no goals