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

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ rtr₂[Component.val cpt][i] = (fun x => v) <$> rtr₁[Component.val cpt][i]
Tactic:
induction u
State after:
case final
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]

case nested
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ 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
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
case final h₁ h₂ => 
  rw [get?_some_to_obj?_some h₁, get?_some_to_obj?_some h₂, Option.map_some]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
case nested h₁ h₂ u hi =>
  have ⟨_, h₁'⟩ := u.obj?_some₁
  have ⟨_, h₂'⟩ := u.obj?_some₂
  rw [obj?_some_nested h₁ h₁', obj?_some_nested h₂ h₂']
  exact h₁' ▸ h₂' ▸ hi
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
rw [get?_some_to_obj?_some h₁, get?_some_to_obj?_some h₂, Option.map_some]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
have ⟨_, h₁'⟩ := u.obj?_some₁
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝
⊢ 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
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
have ⟨_, h₂'⟩ := u.obj?_some₂
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ 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
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
rw [obj?_some_nested h₁ h₁', obj?_some_nested h₂ h₂']
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ some w✝ = (fun x => v) <$> some w✝¹

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ some w✝ = (fun x => v) <$> some w✝¹
Tactic:
exact h₁' ▸ h₂' ▸ hi
State after:
no goals