Theorem: Reactor.LawfulMemUpdate.obj?_preserved (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ rtr₂[Component.val c][j] = rtr₁[Component.val c][j]
Tactic:
cases ho₁ : rtr₁[c][j]
State after:
case none
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none

case some
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none
Tactic:
case none => simp [obj?_none_iff u |>.mp ho₁]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
case some =>
  have ⟨_, ho₂⟩ := obj?_some_iff u |>.mp ⟨_, ho₁⟩ 
  have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
  have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
  simp [ho₂, m₁.lawfulMemUpdate_object_preserved u h m₂]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none
Tactic:
simp [obj?_none_iff u |>.mp ho₁]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
have ⟨_, ho₂⟩ := obj?_some_iff u |>.mp ⟨_, ho₁⟩
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
⊢ rtr₂[Component.val c][j] = some val✝

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
m₂ : Member (Component.val c) j rtr₂
ho₂ : rtr₂[Component.val c][j] = some (Member.object m₂)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
m₂ : Member (Component.val c) j rtr₂
ho₂ : rtr₂[Component.val c][j] = some (Member.object m₂)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Tactic:
simp [ho₂, m₁.lawfulMemUpdate_object_preserved u h m₂]
State after:
no goals