Theorem: proj (Bml/Tableau.lean)

State before:
g : Formula
X : Finset Formula
⊢ g ∈ projection X ↔ □g ∈ X
Tactic:
rw [projection]
State after:
g : Formula
X : Finset Formula
⊢ (g ∈
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ↔
    □g ∈ X

State before:
g : Formula
X : Finset Formula
⊢ (g ∈
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ↔
    □g ∈ X
Tactic:
simp
State after:
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) ↔
    □g ∈ X

State before:
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) ↔
    □g ∈ X
Tactic:
constructor
State after:
case mp
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) →
    □g ∈ X

case mpr
g : Formula
X : Finset Formula
⊢ □g ∈ X →
    ∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g

State before:
case mp
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) →
    □g ∈ X
Tactic:
intro lhs
State after:
case mp
g : Formula
X : Finset Formula
lhs :
  ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
⊢ □g ∈ X

State before:
case mp
g : Formula
X : Finset Formula
lhs :
  ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
⊢ □g ∈ X
Tactic:
rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩
State after:
case mp.intro.intro
g : Formula
X : Finset Formula
boxg : Formula
boxg_in_X : boxg ∈ X
projboxg_is_g :
  (match boxg with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

State before:
case mp.intro.intro
g : Formula
X : Finset Formula
boxg : Formula
boxg_in_X : boxg ∈ X
projboxg_is_g :
  (match boxg with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
cases boxg
State after:
case mp.intro.intro.bottom
g : Formula
X : Finset Formula
boxg_in_X : bottom ∈ X
projboxg_is_g :
  (match bottom with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.atom_prop
g : Formula
X : Finset Formula
a✝ : Char
boxg_in_X : (·a✝) ∈ X
projboxg_is_g :
  (match ·a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.neg
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : ~a✝ ∈ X
projboxg_is_g :
  (match ~a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.And
g : Formula
X : Finset Formula
a✝¹ a✝ : Formula
boxg_in_X : a✝¹⋀a✝ ∈ X
projboxg_is_g :
  (match a✝¹⋀a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

State before:
case mp.intro.intro.bottom
g : Formula
X : Finset Formula
boxg_in_X : bottom ∈ X
projboxg_is_g :
  (match bottom with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.atom_prop
g : Formula
X : Finset Formula
a✝ : Char
boxg_in_X : (·a✝) ∈ X
projboxg_is_g :
  (match ·a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.neg
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : ~a✝ ∈ X
projboxg_is_g :
  (match ~a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.And
g : Formula
X : Finset Formula
a✝¹ a✝ : Formula
boxg_in_X : a✝¹⋀a✝ ∈ X
projboxg_is_g :
  (match a✝¹⋀a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
repeat' aesop
State after:
no goals

State before:
case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
aesop
State after:
no goals

State before:
case mpr
g : Formula
X : Finset Formula
⊢ □g ∈ X →
    ∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g
Tactic:
intro rhs
State after:
case mpr
g : Formula
X : Finset Formula
rhs : □g ∈ X
⊢ ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g

State before:
case mpr
g : Formula
X : Finset Formula
rhs : □g ∈ X
⊢ ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
Tactic:
use □g
State after:
no goals