Theorem: Reactor.LawfulUpdate.obj?_updated (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h : IsEmpty (Member (Component.val cpt) i rtr₁)
e : rtr₁ = rtr₂
⊢ rtr₂[Component.val cpt][i] = (fun x => v) <$> rtr₁[Component.val cpt][i]
Tactic:
subst e
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
h : IsEmpty (Member (Component.val cpt) i rtr₁)
⊢ rtr₁[Component.val cpt][i] = (fun x => v) <$> rtr₁[Component.val cpt][i]

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
h : IsEmpty (Member (Component.val cpt) i rtr₁)
⊢ rtr₁[Component.val cpt][i] = (fun x => v) <$> rtr₁[Component.val cpt][i]
Tactic:
simp [member_isEmpty_obj?_none h]
State after:
no goals