Theorem: Reactor.Wellformed.shared_dep_local
Proof state before:
case in.inp
α : 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.inp, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.inp, id := j }
this :
  rtr[Component.rcn][match Component.rcn with
      | Component.rtr => ↑i₁
      | Component.rcn => i₁
      | Component.val v => i₁] =
    some rcn₁
⊢ c₁ = c₂

case in.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
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.stv, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

case in.act
α : 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.act, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.act, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.act, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.act, id := j }
⊢ c₁ = c₂

case out.out
α : 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.out
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.out, id := j }
⊢ c₁ = c₂

case out.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
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.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

case out.act
α : 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.act, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.act, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.act, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.act, id := j }
⊢ c₁ = c₂
Tactic:
all_goals 
  cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
  all_goals exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
Proof state after:
no goals