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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ rcns e₁ ~ rcns e₂
Tactic:
apply List.perm_ext_iff_of_nodup e₁.rcns_nodup e₂.rcns_nodup |>.mpr
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ ∀ (a : ID), a ∈ rcns e₁ ↔ a ∈ rcns e₂

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ ∀ (a : ID), a ∈ rcns e₁ ↔ a ∈ rcns e₂
Tactic:
intro rcn
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
by_cases hc : rcn ∈ s.progress
State after:
case pos
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂

case neg
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
case pos => simp [e₁.progress_not_mem_rcns hc, e₂.progress_not_mem_rcns hc]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
case neg =>
  constructor <;> intro hm
  case' mp  => have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
  case' mpr => have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
  all_goals exact (Set.mem_union ..).mp h |>.resolve_left hc
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∈ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
simp [e₁.progress_not_mem_rcns hc, e₂.progress_not_mem_rcns hc]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
⊢ rcn ∈ rcns e₁ ↔ rcn ∈ rcns e₂
Tactic:
constructor <;> intro hm
State after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁

State before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
case' mp  => have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
State after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁

State before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
case' mpr => have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
State after:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁

case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

State before:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁

case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Tactic:
all_goals exact (Set.mem_union ..).mp h |>.resolve_left hc
State after:
no goals

State before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
⊢ rcn ∈ rcns e₂
Tactic:
have h := e₂.progress_eq ▸ hp ▸ e₁.rcns_mem_progress hm
State after:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂

State before:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
⊢ rcn ∈ rcns e₁
Tactic:
have h := e₁.progress_eq ▸ hp.symm ▸ e₂.rcns_mem_progress hm
State after:
case mpr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₂
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₁}
⊢ rcn ∈ rcns e₁

State before:
case mp
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn✝ : ID
s : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
rcn : ID
hc : rcn ∉ s.progress
hm : rcn ∈ rcns e₁
h : rcn ∈ s.progress ∪ {a | a ∈ rcns e₂}
⊢ rcn ∈ rcns e₂
Tactic:
exact (Set.mem_union ..).mp h |>.resolve_left hc
State after:
no goals