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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ s₁.progress ⊂ s₂.progress
Tactic:
induction e
State after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ 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
⊢ s₁✝.progress ⊂ s₃✝.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ s₂✝.progress
Tactic:
case single e     => exact e.progress_ssubset
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
⊢ s₁✝.progress ⊂ s₃✝.progress
Tactic:
case trans e _ hi => exact e.progress_ssubset |>.trans hi
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₁✝.progress ⊂ s₂✝.progress
Tactic:
exact e.progress_ssubset
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
⊢ s₁✝.progress ⊂ s₃✝.progress
Tactic:
exact e.progress_ssubset |>.trans hi
State after:
no goals