internlm/Lean-Github huggingface dataset:
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.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₂'
Proof state after:
no goals
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 }
⊢ c₁ = c₂
Tactic:
cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
Proof 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₂
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}
⊢ 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₂
Proof state after:
no goals
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}
⊢ c₁ = c₂
Tactic:
have hc₁' := obj?_some_extend hc₁ hn₁
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✝¹
⊢ c₁ = c₂
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✝¹
⊢ c₁ = c₂
Tactic:
have hc₂' := obj?_some_extend hc₂ hn₂
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✝
⊢ c₁ = c₂
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✝
hj : j✝¹ = j✝
⊢ c₁ = c₂
Tactic:
exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_dep_local
Proof 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₂ ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Wellformed.shared_state_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
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₁
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
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₂
Theorem: Reactor.Wellformed.shared_state_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
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₂
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
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₂
Theorem: Reactor.Wellformed.shared_state_local
Proof 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₂ ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.ext_obj?
Proof state before:
α : Type
rtr₂ : α
inst✝ : Proper α
rtr₁ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
induction rtr₁ using WellFounded.induction generalizing rtr₂
Proof state after:
case nested
α : Type
inst✝ : Proper α
rtr✝ : α
a✝ :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr✝{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr✝ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr✝[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr✝ = rtr₂
Theorem: Reactor.ext_obj?
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
case nested rtr₁ hi =>
  ext1; funext cpt i
  case _ =>
    cases hc₁ : rtr₁{cpt}{i}
    case none => simp [Equivalent.get?_none_iff e |>.mp hc₁]
    case some n₁ =>
      have ⟨n₂, hc₂⟩ := Equivalent.get?_some_iff e |>.mp ⟨_, hc₁⟩ 
      simp [hc₂]
      cases cpt
      case rcn => exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
      case rtr =>
        apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
        intro c _ _ _ ho₁ ho₂
        exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
      all_goals 
        have ho₁ := get?_some_to_obj?_some hc₁
        have ho₂ := get?_some_to_obj?_some hc₂
        exact h ho₁ ho₂
Proof state after:
no goals
Theorem: Reactor.ext_obj?
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
ext1
Proof state after:
case a
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ get? rtr₁ = get? rtr₂
Theorem: Reactor.ext_obj?
Proof state before:
case a
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ get? rtr₁ = get? rtr₂
Tactic:
funext cpt i
Proof state after:
case a.h.h
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
⊢ rtr₁{cpt}{i} = rtr₂{cpt}{i}