Theorem: Reactor.StrictMember.extend_split (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr : α
cpt : Component
i' : ID
rtr' : Component.type α Component.rtr
i : ID
s : StrictMember cpt i' rtr'
h : rtr{Component.rtr}{i} = some rtr'
⊢ extend ↑(split s h).snd ⋯ = nested h s
Tactic:
induction s generalizing rtr i <;> simp [extend]
State after:
case nested
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
a✝¹ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
a_ih✝ : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ a✝¹).2 ⋯ = nested a✝¹ a✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
h' : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
hi : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ h').2 ⋯ = nested h' a✝
Tactic:
case nested h' _ hi => exact hi h'
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
h' : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
hi : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ h').2 ⋯ = nested h' a✝
Tactic:
exact hi h'
State after:
no goals