Theorem: FOL.NV.mem_primeSet_isPrime (FOL/NV/Margaris/Prop.lean)

State before:
F F' : Formula
h1 : F' ∈ F.primeSet
⊢ F'.IsPrime
Tactic:
induction F
State after:
case pred_const_
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_const_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case pred_var_
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case eq_
F' : Formula
a✝¹ a✝ : VarName
h1 : F' ∈ (eq_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case true_
F' : Formula
h1 : F' ∈ true_.primeSet
⊢ F'.IsPrime

case false_
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime

case not_
F' a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ a✝.not_.primeSet
⊢ F'.IsPrime

case imp_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.imp_ a✝).primeSet
⊢ F'.IsPrime

case and_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.and_ a✝).primeSet
⊢ F'.IsPrime

case or_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.or_ a✝).primeSet
⊢ F'.IsPrime

case iff_
F' a✝¹ a✝ : Formula
a_ih✝¹ : F' ∈ a✝¹.primeSet → F'.IsPrime
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (a✝¹.iff_ a✝).primeSet
⊢ F'.IsPrime

case forall_
F' : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (forall_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case exists_
F' : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : F' ∈ a✝.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

case def_
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime

State before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
case pred_const_ | pred_var_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
State after:
no goals

State before:
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime
Tactic:
case true_ | false_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
State after:
no goals

State before:
F' : Formula
x y : VarName
h1 : F' ∈ (eq_ x y).primeSet
⊢ F'.IsPrime
Tactic:
case eq_ x y =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
State after:
no goals

State before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.not_.primeSet
⊢ F'.IsPrime
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.primeSet] at h1
  exact phi_ih h1
State after:
no goals

State before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ (phi.iff_ psi).primeSet
⊢ F'.IsPrime
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp only [Formula.primeSet] at h1
  simp at h1
  tauto
State after:
no goals

State before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝ x).primeSet
⊢ F'.IsPrime
Tactic:
case forall_ x phi | exists_ x phi =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
State after:
no goals

State before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
case def_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
State after:
no goals

State before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ (pred_var_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ {pred_var_ a✝¹ a✝}
⊢ F'.IsPrime

State before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' ∈ {pred_var_ a✝¹ a✝}
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' = pred_var_ a✝¹ a✝
⊢ F'.IsPrime

State before:
F' : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : F' = pred_var_ a✝¹ a✝
⊢ F'.IsPrime
Tactic:
subst h1
State after:
a✝¹ : PredName
a✝ : List VarName
⊢ (pred_var_ a✝¹ a✝).IsPrime

State before:
a✝¹ : PredName
a✝ : List VarName
⊢ (pred_var_ a✝¹ a✝).IsPrime
Tactic:
simp only [Formula.IsPrime]
State after:
no goals

State before:
F' : Formula
h1 : F' ∈ false_.primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' : Formula
h1 : F' ∈ ∅
⊢ F'.IsPrime

State before:
F' : Formula
h1 : F' ∈ ∅
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
no goals

State before:
F' : Formula
x y : VarName
h1 : F' ∈ (eq_ x y).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' : Formula
x y : VarName
h1 : F' ∈ {eq_ x y}
⊢ F'.IsPrime

State before:
F' : Formula
x y : VarName
h1 : F' ∈ {eq_ x y}
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
F' : Formula
x y : VarName
h1 : F' = eq_ x y
⊢ F'.IsPrime

State before:
F' : Formula
x y : VarName
h1 : F' = eq_ x y
⊢ F'.IsPrime
Tactic:
subst h1
State after:
x y : VarName
⊢ (eq_ x y).IsPrime

State before:
x y : VarName
⊢ (eq_ x y).IsPrime
Tactic:
simp only [Formula.IsPrime]
State after:
no goals

State before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.not_.primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet
⊢ F'.IsPrime

State before:
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet
⊢ F'.IsPrime
Tactic:
exact phi_ih h1
State after:
no goals

State before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ (phi.iff_ psi).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∪ psi.primeSet
⊢ F'.IsPrime

State before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∪ psi.primeSet
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∨ F' ∈ psi.primeSet
⊢ F'.IsPrime

State before:
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∨ F' ∈ psi.primeSet
⊢ F'.IsPrime
Tactic:
tauto
State after:
no goals

State before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝ x).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ {exists_ a✝ x}
⊢ F'.IsPrime

State before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ {exists_ a✝ x}
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' = exists_ a✝ x
⊢ F'.IsPrime

State before:
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' = exists_ a✝ x
⊢ F'.IsPrime
Tactic:
subst h1
State after:
a✝ : VarName
x : Formula
phi : exists_ a✝ x ∈ x.primeSet → (exists_ a✝ x).IsPrime
⊢ (exists_ a✝ x).IsPrime

State before:
a✝ : VarName
x : Formula
phi : exists_ a✝ x ∈ x.primeSet → (exists_ a✝ x).IsPrime
⊢ (exists_ a✝ x).IsPrime
Tactic:
simp only [Formula.IsPrime]
State after:
no goals

State before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
Tactic:
simp only [Formula.primeSet] at h1
State after:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ {def_ a✝¹ a✝}
⊢ F'.IsPrime

State before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ {def_ a✝¹ a✝}
⊢ F'.IsPrime
Tactic:
simp at h1
State after:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' = def_ a✝¹ a✝
⊢ F'.IsPrime

State before:
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' = def_ a✝¹ a✝
⊢ F'.IsPrime
Tactic:
subst h1
State after:
a✝¹ : DefName
a✝ : List VarName
⊢ (def_ a✝¹ a✝).IsPrime

State before:
a✝¹ : DefName
a✝ : List VarName
⊢ (def_ a✝¹ a✝).IsPrime
Tactic:
simp only [Formula.IsPrime]
State after:
no goals