Theorem: liftedCIA.restrict_correct (Var/liftedCIA.lean)

State before:
⊢ ∀ (ρ : Config F) (t : TraceRel') (d : Delta'), (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)
Tactic:
intros ρ t d
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (restrict' t d | ρ) = restrict (t | ρ) (d | ρ)
Tactic:
simp [restrict']
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (({x | x ∈ t ∧ (x.1.1, x.2) ∈ d.add} ∪ {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.delete} ∪
        {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.modify}) |
      ρ) =
    restrict (t | ρ) (d | ρ)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (({x | x ∈ t ∧ (x.1.1, x.2) ∈ d.add} ∪ {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.delete} ∪
        {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.modify}) |
      ρ) =
    restrict (t | ρ) (d | ρ)
Tactic:
simp [←Set.setOf_or, Variational.index]
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ vset.index {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify}
      ρ =
    restrict (vset.index t ρ) (indexDelta d ρ)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ vset.index {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify}
      ρ =
    restrict (vset.index t ρ) (indexDelta d ρ)
Tactic:
unfold vset.index
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x =>
      {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify} (x, ρ)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x =>
      {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify} (x, ρ)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Tactic:
simp [setOf, ←(and_or_left)]
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
Tactic:
simp [restrict, indexDelta, allElements, ←Set.setOf_or, index_mem, setOf]
State after:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) = fun x =>
    (x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)

State before:
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) = fun x =>
    (x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)
Tactic:
apply funext
State after:
case h
ρ : Config F
t : TraceRel'
d : Delta'
⊢ ∀ (x : SysEl × GSNEl),
    ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
      ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))

State before:
case h
ρ : Config F
t : TraceRel'
d : Delta'
⊢ ∀ (x : SysEl × GSNEl),
    ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
      ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Tactic:
intros x
State after:
case h
ρ : Config F
t : TraceRel'
d : Delta'
x : SysEl × GSNEl
⊢ ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))

State before:
case h
ρ : Config F
t : TraceRel'
d : Delta'
x : SysEl × GSNEl
⊢ ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
Tactic:
simp [Set.mem_def]
State after:
no goals