internlm/Lean-Github huggingface dataset:
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
case update.notMem
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u✝ : LawfulMemUpdate cpt i v rtr rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂

case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
all_goals exact ‹IsEmpty _›.elim $ Member.strict ‹LawfulMemUpdate ..›.member₁
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝¹ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝¹ : rtr = rtr₁
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₂
⊢ rtr₁ = rtr₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
exact u₁.unique u₂
Proof state after:
no goals
Theorem: Reactor.LawfulUpdate.unique
Proof state before:
case notMem.update
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
h✝ : IsEmpty (Member (Component.val cpt) i rtr)
eq✝ : rtr = rtr₁
u✝ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
exact ‹IsEmpty _›.elim $ Member.strict ‹LawfulMemUpdate ..›.member₁
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
d : j₁ <[rtr₂] j₂
⊢ j₁ <[rtr₁] j₂
Tactic:
induction d with
| prio h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact prio h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| depOverlap h₁ h₂ =>
  exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
| mutNorm h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact mutNorm h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| mutNest h₁ h₂ h₃ _ h₄ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  have ⟨_, h₂'⟩ := get?_some_iff e (cpt := .rtr) |>.mpr ⟨_, h₂⟩
  have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
  exact mutNest h₁' h₂' (get?_rcn_eq e ▸ h₃) ‹_› h₄'
| trans _ _ d₁ d₂ =>
  exact trans d₁ d₂
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : 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
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
Proof state after:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : 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
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ i₁✝ <[rtr₁] i₂✝
Theorem: Dependency.equiv
Proof state before:
case prio
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : 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
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{i₁✝} = some rcn₁✝
h₃ : con✝{Component.rcn}{i₂✝} = some rcn₂✝
a✝¹ : Reaction.Mutates rcn₁✝ ↔ Reaction.Mutates rcn₂✝
a✝ : rcn₁✝.prio > rcn₂✝.prio
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
exact prio h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
case depOverlap
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
h₁ : rtr₂[Component.rcn][i₁✝] = some rcn₁✝
h₂ : rtr₂[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ <[rtr₁] i₂✝
Tactic:
exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
⊢ iₘ✝ <[rtr₁] iₙ✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
Proof state after:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ iₘ✝ <[rtr₁] iₙ✝
Theorem: Dependency.equiv
Proof state before:
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ iₘ✝ <[rtr₁] iₙ✝
Tactic:
exact mutNorm h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
Proof state after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ rtr₁✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Theorem: Dependency.equiv
Proof state before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ rtr₁✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have ⟨_, h₂'⟩ := get?_some_iff e (cpt := .rtr) |>.mpr ⟨_, h₂⟩
Proof state after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Theorem: Dependency.equiv
Proof state before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
Proof state after:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
h₄' : iᵣ✝ ∈ w✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝
Theorem: Dependency.equiv
Proof state before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
h₄' : iᵣ✝ ∈ w✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝
Tactic:
exact mutNest h₁' h₂' (get?_rcn_eq e ▸ h₃) ‹_› h₄'
Proof state after:
no goals
Theorem: Dependency.equiv
Proof state before:
case trans
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr₂] i₂✝
a✝ : i₂✝ <[rtr₂] i₃✝
d₁ : i₁✝ <[rtr₁] i₂✝
d₂ : i₂✝ <[rtr₁] i₃✝
⊢ i₁✝ <[rtr₁] i₃✝
Tactic:
exact trans d₁ d₂
Proof state after:
no goals
Theorem: Dependency.mem₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
d : rcn₁ <[rtr] rcn₂
⊢ rcn₁ ∈ rtr[Component.rcn]
Tactic:
induction d <;> try exact Partial.mem_iff.mpr ⟨_, obj?_some_extend ‹_› ‹_›⟩
Proof state after:
case depOverlap
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
a✝⁴ : rtr[Component.rcn][i₁✝] = some rcn₁✝
a✝³ : rtr[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ ∈ rtr[Component.rcn]

case trans
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr] i₂✝
a✝ : i₂✝ <[rtr] i₃✝
a_ih✝¹ : i₁✝ ∈ rtr[Component.rcn]
a_ih✝ : i₂✝ ∈ rtr[Component.rcn]
⊢ i₁✝ ∈ rtr[Component.rcn]
Theorem: Dependency.mem₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
a✝⁴ : rtr[Component.rcn][i₁✝] = some rcn₁✝
a✝³ : rtr[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ ∈ rtr[Component.rcn]
Tactic:
case depOverlap => exact Partial.mem_iff.mpr ⟨_, ‹_›⟩
Proof state after:
no goals
Theorem: Dependency.mem₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr] i₂✝
a✝ : i₂✝ <[rtr] i₃✝
a_ih✝¹ : i₁✝ ∈ rtr[Component.rcn]
a_ih✝ : i₂✝ ∈ rtr[Component.rcn]
⊢ i₁✝ ∈ rtr[Component.rcn]
Tactic:
case trans => assumption
Proof state after:
no goals
Theorem: Dependency.mem₁
Proof state before:
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
a✝⁴ : rtr[Component.rtr][i✝] = some rtr₁✝
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝¹ : Reaction.Mutates m✝
a✝ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
⊢ iₘ✝ ∈ rtr[Component.rcn]
Tactic:
exact Partial.mem_iff.mpr ⟨_, obj?_some_extend ‹_› ‹_›⟩
Proof state after:
no goals
Theorem: Dependency.mem₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ : ID
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
a✝⁴ : rtr[Component.rcn][i₁✝] = some rcn₁✝
a✝³ : rtr[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ ∈ rtr[Component.rcn]
Tactic:
exact Partial.mem_iff.mpr ⟨_, ‹_›⟩
Proof state after:
no goals
Theorem: Dependency.mem₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
rcn₁ rcn₂ i₁✝ i₂✝ i₃✝ : ID
a✝¹ : i₁✝ <[rtr] i₂✝
a✝ : i₂✝ <[rtr] i₃✝
a_ih✝¹ : i₁✝ ∈ rtr[Component.rcn]
a_ih✝ : i₂✝ ∈ rtr[Component.rcn]
⊢ i₁✝ ∈ rtr[Component.rcn]
Tactic:
assumption
Proof state after:
no goals
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ Acyclic rtr ↔ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
apply not_iff_not.mp
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ ¬Acyclic rtr ↔ ¬∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Theorem: Dependency.Acyclic.iff_mem_acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ ¬Acyclic rtr ↔ ¬∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
simp [Acyclic]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr✝ rtr₁ rtr : α
⊢ (∃ x, x <[rtr] x) ↔ ∃ x ∈ rtr[Component.rcn], x <[rtr] x