Theorem: Reactor.Wellformed.shared_state_local (ReactorModel/Objects/Reactor/Theorems/Proper.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
⊢ c₁ = c₂
Tactic:
have hv₁ := wf.valid_deps hc₁ hr₁ hd₁
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂
Tactic:
have hv₂ := wf.valid_deps hc₂ hr₂ hd₂
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂
Tactic:
cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
State after:
case mut.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case mut.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

State before:
case mut.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case mut.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂
Tactic:
all_goals exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
State after:
no goals

State before:
case norm.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂
Tactic:
exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
State after:
no goals