Theorem: Reactor.Wellformed.shared_dep_local
Proof 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.out, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.out, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
j✝¹ : ID
con✝¹ : Component.type (Component.type α Component.rtr) Component.rtr
hn₁ : con₁{Component.rtr}{j✝¹} = some con✝¹
hj₁ : j ∈ con✝¹{Component.out}
j✝ : ID
con✝ : Component.type (Component.type α Component.rtr) Component.rtr
hn₂ : con₂{Component.rtr}{j✝} = some con✝
hj₂ : j ∈ con✝{Component.out}
hc₁' :
  rtr[Component.rtr][match Component.rtr with
      | Component.rtr => ↑j✝¹
      | Component.rcn => j✝¹
      | Component.val v => j✝¹] =
    some con✝¹
hc₂' :
  rtr[Component.rtr][match Component.rtr with
      | Component.rtr => ↑j✝
      | Component.rcn => j✝
      | Component.val v => j✝] =
    some con✝
⊢ c₁ = c₂
Tactic:
have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
Proof 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.out, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.out, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
j✝¹ : ID
con✝¹ : Component.type (Component.type α Component.rtr) Component.rtr
hn₁ : con₁{Component.rtr}{j✝¹} = some con✝¹
hj₁ : j ∈ con✝¹{Component.out}
j✝ : ID
con✝ : Component.type (Component.type α Component.rtr) Component.rtr
hn₂ : con₂{Component.rtr}{j✝} = some con✝
hj₂ : j ∈ con✝{Component.out}
hc₁' :
  rtr[Component.rtr][match Component.rtr with
      | Component.rtr => ↑j✝¹
      | Component.rcn => j✝¹
      | Component.val v => j✝¹] =
    some con✝¹
hc₂' :
  rtr[Component.rtr][match Component.rtr with
      | Component.rtr => ↑j✝
      | Component.rcn => j✝
      | Component.val v => j✝] =
    some con✝
hj :
  (match Component.rtr with
    | Component.rtr => ↑j✝¹
    | Component.rcn => j✝¹
    | Component.val v => j✝¹) =
    match Component.rtr with
    | Component.rtr => ↑j✝
    | Component.rcn => j✝
    | Component.val v => j✝
⊢ c₁ = c₂