internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.varSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
Tactic:
simp
Proof state after:
v : VarName
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∨ v ∈ psi.varSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∪ {x}
Tactic:
simp
Proof state after:
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∨ v = x
Theorem: FOL.NV.occursIn_iff_mem_varSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∨ v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
F : Formula
⊢ isBoundIn v F ↔ v ∈ F.boundVarSet
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isBoundIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).boundVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isBoundIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).boundVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isBoundIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).boundVarSet

case true_
v : VarName
⊢ isBoundIn v true_ ↔ v ∈ true_.boundVarSet

case false_
v : VarName
⊢ isBoundIn v false_ ↔ v ∈ false_.boundVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v a✝.not_ ↔ v ∈ a✝.not_.boundVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).boundVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).boundVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).boundVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).boundVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).boundVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ ↔ v ∈ a✝.boundVarSet
⊢ isBoundIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).boundVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isBoundIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ False ↔ v ∈ ∅
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v x y : VarName
⊢ False ↔ v ∈ ∅
Tactic:
case eq_ x y =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ isBoundIn v phi ↔ v ∈ phi.boundVarSet
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
psi_ih : isBoundIn v psi ↔ v ∈ psi.boundVarSet
⊢ isBoundIn v phi ∨ isBoundIn v psi ↔ v ∈ phi.boundVarSet ∪ psi.boundVarSet
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
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∪ {x}
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isBoundIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
Tactic:
simp only [isBoundIn]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ v ∈ (def_ a✝¹ a✝).boundVarSet
Tactic:
simp only [Formula.boundVarSet]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ v ∈ ∅
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ False ↔ v ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v x y : VarName
⊢ False ↔ v ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ isBoundIn v phi ↔ v ∈ phi.boundVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
psi_ih : isBoundIn v psi ↔ v ∈ psi.boundVarSet
⊢ isBoundIn v phi ∨ isBoundIn v psi ↔ v ∈ phi.boundVarSet ∪ psi.boundVarSet
Tactic:
simp
Proof state after:
v : VarName
phi psi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
psi_ih : isBoundIn v psi ↔ v ∈ psi.boundVarSet
⊢ isBoundIn v phi ∨ isBoundIn v psi ↔ v ∈ phi.boundVarSet ∨ v ∈ psi.boundVarSet
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
psi_ih : isBoundIn v psi ↔ v ∈ psi.boundVarSet
⊢ isBoundIn v phi ∨ isBoundIn v psi ↔ v ∈ phi.boundVarSet ∨ v ∈ psi.boundVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∪ {x}
Tactic:
simp
Proof state after:
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∨ v = x
Theorem: FOL.NV.isBoundIn_iff_mem_boundVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∨ v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
F : Formula
⊢ isFreeIn v F ↔ v ∈ F.freeVarSet
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isFreeIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).freeVarSet

case true_
v : VarName
⊢ isFreeIn v true_ ↔ v ∈ true_.freeVarSet

case false_
v : VarName
⊢ isFreeIn v false_ ↔ v ∈ false_.freeVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝.not_ ↔ v ∈ a✝.not_.freeVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).freeVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).freeVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).freeVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).freeVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).freeVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).freeVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
case eq_ x y =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ isFreeIn v phi ↔ v ∈ phi.freeVarSet
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
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
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet \ {x}
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [isFreeIn]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ (def_ a✝¹ a✝).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ v ∈ a✝ ↔ v ∈ a✝.toFinset
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
X : DefName
xs : List VarName
⊢ v ∈ xs ↔ v ∈ xs.toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v x y : VarName
⊢ v = x ∨ v = y ↔ v ∈ {x, y}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
⊢ False ↔ v ∈ ∅
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ isFreeIn v phi ↔ v ∈ phi.freeVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
Tactic:
simp
Proof state after:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∨ v ∈ psi.freeVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet \ {x}
Tactic:
simp
Proof state after:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet ∧ ¬v = x
Theorem: FOL.NV.isFreeIn_iff_mem_freeVarSet
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi ↔ v ∈ phi.freeVarSet
⊢ ¬v = x ∧ isFreeIn v phi ↔ v ∈ phi.freeVarSet ∧ ¬v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
F : Formula
h1 : isFreeIn v F
⊢ isFreeInInd v F
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_const_ a✝¹ a✝)
⊢ isFreeInInd v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isFreeIn v (pred_var_ a✝¹ a✝)
⊢ isFreeInInd v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isFreeIn v (eq_ a✝¹ a✝)
⊢ isFreeInInd v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isFreeIn v true_
⊢ isFreeInInd v true_

case false_
v : VarName
h1 : isFreeIn v false_
⊢ isFreeInInd v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v a✝.not_
⊢ isFreeInInd v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.imp_ a✝)
⊢ isFreeInInd v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.and_ a✝)
⊢ isFreeInInd v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.or_ a✝)
⊢ isFreeInInd v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ → isFreeInInd v a✝¹
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (a✝¹.iff_ a✝)
⊢ isFreeInInd v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (forall_ a✝¹ a✝)
⊢ isFreeInInd v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ → isFreeInInd v a✝
h1 : isFreeIn v (exists_ a✝¹ a✝)
⊢ isFreeInInd v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ isFreeInInd v (def_ a✝¹ a✝)
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y | def_ X xs =>
  first | exact isFreeInInd.pred_const_ X xs h1 | exact isFreeInInd.pred_var_ X xs h1 | exact isFreeInInd.eq_ x y h1 | exact isFreeInInd.def_ X xs h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi.not_
Tactic:
case not_ phi phi_ih =>
  apply isFreeInInd.not_
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h1 : isFreeIn v phi ∨ isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
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 =>
  cases h1
  case inl c1 =>
    first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
    exact phi_ih c1
  case inr c1 =>
    first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
    exact psi_ih c1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isFreeIn v (def_ a✝¹ a✝)
⊢ isFreeInInd v (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∈ a✝
⊢ isFreeInInd v (def_ a✝¹ a✝)
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
first | exact isFreeInInd.pred_const_ X xs h1 | exact isFreeInInd.pred_var_ X xs h1 | exact isFreeInInd.eq_ x y h1 | exact isFreeInInd.def_ X xs h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
X : PredName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (pred_const_ X xs)
Tactic:
exact isFreeInInd.pred_const_ X xs h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
X : PredName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (pred_var_ X xs)
Tactic:
exact isFreeInInd.pred_var_ X xs h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v x y : VarName
h1 : v = x ∨ v = y
⊢ isFreeInInd v (eq_ x y)
Tactic:
exact isFreeInInd.eq_ x y h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
X : DefName
xs : List VarName
h1 : v ∈ xs
⊢ isFreeInInd v (def_ X xs)
Tactic:
exact isFreeInInd.def_ X xs h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi.not_
Tactic:
apply isFreeInInd.not_
Proof state after:
case a
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case a
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h1 : isFreeIn v phi ∨ isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
cases h1
Proof state after:
case inl
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)

case inr
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
case inl c1 =>
  first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
  exact phi_ih c1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
case inr c1 =>
  first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
  exact psi_ih c1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih c1
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.imp_ psi)
Tactic:
apply isFreeInInd.imp_left_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.and_ psi)
Tactic:
apply isFreeInInd.and_left_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.or_ psi)
Tactic:
apply isFreeInInd.or_left_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
apply isFreeInInd.iff_left_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Tactic:
exact psi_ih c1
Proof state after:
no goals