Theorem: Reactor.Wellformed.shared_dep_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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
⊢ c₁ = c₂
Tactic:
by_cases hi : i₁ = i₂
State after:
case pos
α : 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂

case neg
α : 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂
Tactic:
case pos => exact get?_some_rtr_eq hc₁ hc₂ (hi ▸ hr₁) hr₂
State after:
no goals

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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ c₁ = c₂
Tactic:
case neg =>
  have hv₁ := wf.valid_deps hc₁ hr₁ hd₁
  have hv₂ := wf.valid_deps hc₂ hr₂ hd₂
  cases k <;> cases cpt <;> try cases ‹Kind› 
  have := obj?_some_extend hc₁ hr₁
  case out.inp => 
    have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
    exact absurd hd₂ hd₂'
  case in.out =>
    cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
    case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
      have hc₁' := obj?_some_extend hc₁ hn₁
      have hc₂' := obj?_some_extend hc₂ hn₂
      have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
      injection hj with hj
      exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂ 
  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₂ ‹_› ‹_›
State after:
no goals

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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : i₁ = i₂
⊢ c₁ = c₂
Tactic:
exact get?_some_rtr_eq hc₁ hc₂ (hi ▸ hr₁) hr₂
State after:
no goals

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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k { cpt := cpt, 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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k { cpt := cpt, id := j }
⊢ c₁ = c₂
Tactic:
cases k <;> cases cpt <;> try cases ‹Kind›
State after:
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 }
⊢ c₁ = c₂

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

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 }
⊢ c₁ = c₂

case in.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.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 }
⊢ 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.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.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, 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:
have := obj?_some_extend hc₁ hr₁
State after:
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.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.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 }
⊢ 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.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.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, 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₂

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.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂
Tactic:
case out.inp => 
  have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
  exact absurd hd₂ hd₂'
State after:
no goals

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 }
⊢ c₁ = c₂
Tactic:
case in.out =>
  cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
  case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
    have hc₁' := obj?_some_extend hc₁ hn₁
    have hc₂' := obj?_some_extend hc₂ hn₂
    have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
    injection hj with hj
    exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂
State after:
no goals

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₂ ‹_› ‹_›
State after:
no goals

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.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂
Tactic:
have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi 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
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.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
hd₂' : { cpt := Component.Valued.inp, id := j } ∉ rcn₂.deps Kind.out
⊢ 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
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.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
hd₂' : { cpt := Component.Valued.inp, id := j } ∉ rcn₂.deps Kind.out
⊢ c₁ = c₂
Tactic:
exact absurd hd₂ hd₂'
State after:
no goals

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 }
⊢ c₁ = c₂
Tactic:
cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
State after:
case norm.norm.nestedOut.nestedOut
α : 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
a✝³ : con₁{Component.rtr}{j✝¹} = some con✝¹
a✝² : j ∈ con✝¹{Component.out}
j✝ : ID
con✝ : Component.type (Component.type α Component.rtr) Component.rtr
a✝¹ : con₂{Component.rtr}{j✝} = some con✝
a✝ : j ∈ con✝{Component.out}
⊢ 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
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}
⊢ c₁ = c₂
Tactic:
case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
  have hc₁' := obj?_some_extend hc₁ hn₁
  have hc₂' := obj?_some_extend hc₂ hn₂
  have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
  injection hj with hj
  exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂
State after:
no goals

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}
⊢ c₁ = c₂
Tactic:
have hc₁' := obj?_some_extend hc₁ hn₁
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✝¹
⊢ 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
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✝¹
⊢ c₁ = c₂
Tactic:
have hc₂' := obj?_some_extend hc₂ hn₂
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✝
⊢ 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
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₂
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₂

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✝
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₂
Tactic:
injection hj with hj
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 : j✝¹ = 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
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 : j✝¹ = j✝
⊢ c₁ = c₂
Tactic:
exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂
State after:
no goals

State before:
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:
cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
State after:
case out.act.mut.mut.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.mut.norm.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.norm.mut.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.norm.norm.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

State before:
case out.act.mut.mut.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.mut.norm.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.norm.mut.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂

case out.act.norm.norm.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂
Tactic:
all_goals exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
State after:
no goals

State before:
case out.act.norm.norm.act.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 }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.act}
a✝ : j ∈ con₂{Component.act}
⊢ c₁ = c₂
Tactic:
exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
State after:
no goals