Theorem: Reactor.LawfulUpdate.unique (ReactorModel/Objects/Reactor/Theorems/Readable.lean)

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulUpdate cpt i v rtr rtr₁
u₂ : LawfulUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
cases u₁ <;> cases u₂
State after:
case update.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝¹ : LawfulMemUpdate cpt i v rtr rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case update.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝ : LawfulMemUpdate cpt i v rtr rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂

case notMem.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂
Tactic:
case notMem.notMem => simp_all
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
case update.update u₁ u₂ => exact u₁.unique u₂
State after:
no goals

State before:
case update.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝ : LawfulMemUpdate cpt i v rtr rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
all_goals exact ‹IsEmpty _›.elim $ Member.strict ‹LawfulMemUpdate ..›.member₁
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂
Tactic:
simp_all
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
exact u₁.unique u₂
State after:
no goals

State before:
case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
exact ‹IsEmpty _›.elim $ Member.strict ‹LawfulMemUpdate ..›.member₁
State after:
no goals