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

State before:
⊢ ∀ (g : GSN') (recheck revise : vset F GSNEl) (ρ : Config F),
    (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
intros g recheck revise ρ
State after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)

State before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
simp [createAnnotation', Set.image]
State after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (({x | ∃ a b, (a, b) ∈ recheck ∧ ((a, Annotation.Recheck), b) = x} ∪
          {x | ∃ a b, (a, b) ∈ revise ∧ ((a, Annotation.Revise), b) = x} ∪
        {x | ∃ a b, ((a, b) ∈ g ∧ ¬((a, b) ∈ recheck ∨ (a, b) ∈ revise)) ∧ ((a, Annotation.Reuse), b) = x}) |
      ρ) =
    createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)

State before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (({x | ∃ a b, (a, b) ∈ recheck ∧ ((a, Annotation.Recheck), b) = x} ∪
          {x | ∃ a b, (a, b) ∈ revise ∧ ((a, Annotation.Revise), b) = x} ∪
        {x | ∃ a b, ((a, b) ∈ g ∧ ¬((a, b) ∈ recheck ∨ (a, b) ∈ revise)) ∧ ((a, Annotation.Reuse), b) = x}) |
      ρ) =
    createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
Tactic:
simp [←Set.setOf_or, Variational.index]
State after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ vset.index
      {a |
        ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
            ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
          ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
      ρ =
    createAnnotation (vset.index g ρ) (vset.index recheck ρ) (vset.index revise ρ)

State before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ vset.index
      {a |
        ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
            ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
          ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
      ρ =
    createAnnotation (vset.index g ρ) (vset.index recheck ρ) (vset.index revise ρ)
Tactic:
unfold vset.index
State after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      {a |
          ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
              ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
            ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
        (x, ρ)) =
    createAnnotation (fun x => g (x, ρ)) (fun x => recheck (x, ρ)) fun x => revise (x, ρ)

State before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      {a |
          ((∃ a_1 b, (a_1, b) ∈ recheck ∧ ((a_1, Annotation.Recheck), b) = a) ∨
              ∃ a_1 b, (a_1, b) ∈ revise ∧ ((a_1, Annotation.Revise), b) = a) ∨
            ∃ a_1 b, ((a_1, b) ∈ g ∧ ¬((a_1, b) ∈ recheck ∨ (a_1, b) ∈ revise)) ∧ ((a_1, Annotation.Reuse), b) = a}
        (x, ρ)) =
    createAnnotation (fun x => g (x, ρ)) (fun x => recheck (x, ρ)) fun x => revise (x, ρ)
Tactic:
simp [createAnnotation, Set.image, ←Set.setOf_or, setOf]
State after:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      ((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    ((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
        ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
      fun x =>
      ∃ a,
        ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
          (a, Annotation.Reuse) = x

State before:
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (fun x =>
      ((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    ((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
        ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
      fun x =>
      ∃ a,
        ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
          (a, Annotation.Reuse) = x
Tactic:
apply funext
State after:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ ∀ (x : GSNEl × Annotation),
    (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
      (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
            ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
          fun x =>
          ∃ a,
            ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
              (a, Annotation.Reuse) = x)
        x

State before:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ ∀ (x : GSNEl × Annotation),
    (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
        ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
      (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
            ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
          fun x =>
          ∃ a,
            ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
              (a, Annotation.Reuse) = x)
        x
Tactic:
intros x
State after:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
x : GSNEl × Annotation
⊢ (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
      ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
          ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
        fun x =>
        ∃ a,
          ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
            (a, Annotation.Reuse) = x)
      x

State before:
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
x : GSNEl × Annotation
⊢ (((∃ a, (a, ρ) ∈ recheck ∧ (a, Annotation.Recheck) = x) ∨ ∃ a, (a, ρ) ∈ revise ∧ (a, Annotation.Revise) = x) ∨
      ∃ a, ((a, ρ) ∈ g ∧ ¬((a, ρ) ∈ recheck ∨ (a, ρ) ∈ revise)) ∧ (a, Annotation.Reuse) = x) =
    (((fun x => ∃ a ∈ fun x => recheck (x, ρ), (a, Annotation.Recheck) = x) ∪ fun x =>
          ∃ a ∈ fun x => revise (x, ρ), (a, Annotation.Revise) = x) ∪
        fun x =>
        ∃ a,
          ((a ∈ fun x => g (x, ρ)) ∧ ¬((a ∈ fun x => recheck (x, ρ)) ∨ a ∈ fun x => revise (x, ρ))) ∧
            (a, Annotation.Reuse) = x)
      x
Tactic:
simp[Set.mem_def, Set.union_def, setOf]
State after:
no goals