Theorem: proj (Pdl/Tableau.lean)

State before:
g : Formula
A : ℕ
X : List Formula
⊢ g ∈ projection A X ↔ (⌈·A⌉g) ∈ X
Tactic:
induction X
State after:
case nil
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []

case cons
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝

State before:
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []
Tactic:
case nil =>
  simp only [projection, formProjection, beq_iff_eq, List.map_nil, List.not_mem_nil, iff_false]
  exact List.count_eq_zero.mp rfl
State after:
no goals

State before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
Tactic:
case cons =>
  simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
  rw [List.reduceOption_mem_iff]
  aesop
State after:
no goals

State before:
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []
Tactic:
simp only [projection, formProjection, beq_iff_eq, List.map_nil, List.not_mem_nil, iff_false]
State after:
g : Formula
A : ℕ
⊢ g ∉ [].reduceOption

State before:
g : Formula
A : ℕ
⊢ g ∉ [].reduceOption
Tactic:
exact List.count_eq_zero.mp rfl
State after:
no goals

State before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
Tactic:
simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
State after:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈
      ((match A, head✝ with
          | A, ⌈·B⌉φ => if A = B then some φ else none
          | x, x_1 => none) ::
          List.map
            (fun x =>
              match A, x with
              | A, ⌈·B⌉φ => if A = B then some φ else none
              | x, x_1 => none)
            tail✝).reduceOption ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝

State before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈
      ((match A, head✝ with
          | A, ⌈·B⌉φ => if A = B then some φ else none
          | x, x_1 => none) ::
          List.map
            (fun x =>
              match A, x with
              | A, ⌈·B⌉φ => if A = B then some φ else none
              | x, x_1 => none)
            tail✝).reduceOption ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Tactic:
rw [List.reduceOption_mem_iff]
State after:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ some g ∈
      (match A, head✝ with
        | A, ⌈·B⌉φ => if A = B then some φ else none
        | x, x_1 => none) ::
        List.map
          (fun x =>
            match A, x with
            | A, ⌈·B⌉φ => if A = B then some φ else none
            | x, x_1 => none)
          tail✝ ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝

State before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ some g ∈
      (match A, head✝ with
        | A, ⌈·B⌉φ => if A = B then some φ else none
        | x, x_1 => none) ::
        List.map
          (fun x =>
            match A, x with
            | A, ⌈·B⌉φ => if A = B then some φ else none
            | x, x_1 => none)
          tail✝ ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Tactic:
aesop
State after:
no goals