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

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
u : LawfulUpdate cpt i v rtr₁ rtr₂
s : StrictMember c j rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s u
Tactic:
cases u
State after:
case update
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u✝ : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u✝)

case notMem
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)
Tactic:
case notMem   => cases ‹_ = _›; apply refl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u)
Tactic:
case update u => exact fromLawfulMemUpdate u s
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)
Tactic:
cases ‹_ = _›
State after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component
j : ID
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
s : StrictMember c j rtr₁
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ ⋯)

State before:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component
j : ID
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
s : StrictMember c j rtr₁
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ ⋯)
Tactic:
apply refl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u)
Tactic:
exact fromLawfulMemUpdate u s
State after:
no goals