Theorem: Execution.State.Allows.congr (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
constructor <;> intro ⟨hm, hd, hu⟩
State after:
case mp
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ Allows s₂ i

case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i

State before:
case mp
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ Allows s₂ i

case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i
Tactic:
all_goals
  exact {
    mem := by first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
    deps := equiv_eq_dependencies hr ▸ hp ▸ hd
    unprocessed := hp ▸ hu
  }
State after:
no goals

State before:
case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i
Tactic:
exact {
  mem := by first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
  deps := equiv_eq_dependencies hr ▸ hp ▸ hd
  unprocessed := hp ▸ hu
}
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ i ∈ s₁.rtr[Component.rcn]
Tactic:
first | exact Equivalent.mem_iff hr |>.mp hm | exact Equivalent.mem_iff hr |>.mpr hm
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ i ∈ s₂.rtr[Component.rcn]
Tactic:
exact Equivalent.mem_iff hr |>.mp hm
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ i ∈ s₁.rtr[Component.rcn]
Tactic:
exact Equivalent.mem_iff hr |>.mpr hm
State after:
no goals