Theorem: Dependency.mem₁ (ReactorModel/Execution/Theorems/Dependency.lean)

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 ‹_› ‹_›⟩
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]

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

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
State after:
no goals

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

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

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
State after:
no goals