Theorem: Execution.Instantaneous.Step.TC.progress_eq (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ s₂.progress = s₁.progress ∪ {a | a ∈ rcns e}
Tactic:
induction e <;> simp [rcns]
State after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn a✝) s₁✝.progress

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn a✝¹ ∨ a ∈ rcns a✝}

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress
Tactic:
case single e     => exact e.progress_eq
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
case trans e _ hi => simp [hi, e.progress_eq]; apply Set.insert_union'
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress
Tactic:
exact e.progress_eq
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ s₃✝.progress = s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
simp [hi, e.progress_eq]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ Set.insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress ∪ {a | a ∈ rcns a✝} =
    s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : s₃✝.progress = s₂✝.progress ∪ {a | a ∈ rcns a✝}
⊢ Set.insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress ∪ {a | a ∈ rcns a✝} =
    s₁✝.progress ∪ {a | a = Execution.Instantaneous.Step.rcn e ∨ a ∈ rcns a✝}
Tactic:
apply Set.insert_union'
State after:
no goals