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

State before:
α : Type
inst✝ : Reactor α
rtr : α
i : ID
cpt : Component
j : ID
o : Component.type (Component.type α Component.rtr) cpt
o' : Component.type α cpt
s : StrictMember Component.rtr i rtr
h : object s{cpt}{j} = some o
hf : rtr{cpt}{j} = some o'
⊢ extend s h ≠ final hf
Tactic:
cases s <;> simp [extend]
State after:
no goals