Theorem: MM0.sub_preserves_empty_meta_var_set (FOL/MM0/MM0.lean)

State before:
F : Formula
σ : Instantiation
τ : MetaInstantiation
h1 : F.metaVarSet = ∅
⊢ (sub σ τ F).metaVarSet = ∅
Tactic:
induction F
State after:
case meta_var_
σ : Instantiation
τ : MetaInstantiation
a✝ : MetaVarName
h1 : (meta_var_ a✝).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ a✝)).metaVarSet = ∅

case pred_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_ a✝¹ a✝).metaVarSet = ∅
⊢ (sub σ τ (pred_ a✝¹ a✝)).metaVarSet = ∅

case eq_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).metaVarSet = ∅
⊢ (sub σ τ (eq_ a✝¹ a✝)).metaVarSet = ∅

case true_
σ : Instantiation
τ : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ (sub σ τ true_).metaVarSet = ∅

case not_
σ : Instantiation
τ : MetaInstantiation
a✝ : Formula
a_ih✝ : a✝.metaVarSet = ∅ → (sub σ τ a✝).metaVarSet = ∅
h1 : a✝.not_.metaVarSet = ∅
⊢ (sub σ τ a✝.not_).metaVarSet = ∅

case imp_
σ : Instantiation
τ : MetaInstantiation
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.metaVarSet = ∅ → (sub σ τ a✝¹).metaVarSet = ∅
a_ih✝ : a✝.metaVarSet = ∅ → (sub σ τ a✝).metaVarSet = ∅
h1 : (a✝¹.imp_ a✝).metaVarSet = ∅
⊢ (sub σ τ (a✝¹.imp_ a✝)).metaVarSet = ∅

case forall_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.metaVarSet = ∅ → (sub σ τ a✝).metaVarSet = ∅
h1 : (forall_ a✝¹ a✝).metaVarSet = ∅
⊢ (sub σ τ (forall_ a✝¹ a✝)).metaVarSet = ∅

case def_
σ : Instantiation
τ : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).metaVarSet = ∅
⊢ (sub σ τ (def_ a✝¹ a✝)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Tactic:
case meta_var_ X =>
  unfold Formula.metaVarSet at h1
  simp at h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : (pred_ X xs).metaVarSet = ∅
⊢ (sub σ τ (pred_ X xs)).metaVarSet = ∅
Tactic:
case pred_ X xs =>
  rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ (sub σ τ (eq_ x y)).metaVarSet = ∅
Tactic:
case eq_ x y =>
  rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ (sub σ τ true_).metaVarSet = ∅
Tactic:
case true_ =>
  rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.not_.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅
Tactic:
case not_ phi phi_ih =>
  unfold Formula.metaVarSet at h1
  unfold sub
  unfold Formula.metaVarSet
  exact phi_ih h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : (forall_ x phi).metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅
Tactic:
case forall_ x phi phi_ih =>
  unfold Formula.metaVarSet at h1
  unfold sub
  unfold Formula.metaVarSet
  exact phi_ih h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : (def_ X xs).metaVarSet = ∅
⊢ (sub σ τ (def_ X xs)).metaVarSet = ∅
Tactic:
case def_ X xs =>
  rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet at h1
State after:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Tactic:
simp at h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : (pred_ X xs).metaVarSet = ∅
⊢ (sub σ τ (pred_ X xs)).metaVarSet = ∅
Tactic:
rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ (sub σ τ (eq_ x y)).metaVarSet = ∅
Tactic:
rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ (sub σ τ true_).metaVarSet = ∅
Tactic:
rfl
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.not_.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet at h1
State after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅
Tactic:
unfold sub
State after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_.metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_.metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
State after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Tactic:
exact phi_ih h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : (phi.imp_ psi).metaVarSet = ∅
⊢ (sub σ τ (phi.imp_ psi)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet at h1
State after:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet ∪ psi.metaVarSet = ∅
⊢ (sub σ τ (phi.imp_ psi)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet ∪ psi.metaVarSet = ∅
⊢ (sub σ τ (phi.imp_ psi)).metaVarSet = ∅
Tactic:
simp only [Finset.union_eq_empty] at h1
State after:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ (phi.imp_ psi)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ (phi.imp_ psi)).metaVarSet = ∅
Tactic:
unfold sub
State after:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ ((sub σ τ phi).imp_ (sub σ τ psi)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ ((sub σ τ phi).imp_ (sub σ τ psi)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
State after:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet ∪ (sub σ τ psi).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet ∪ (sub σ τ psi).metaVarSet = ∅
Tactic:
cases h1
State after:
case intro
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
left✝ : phi.metaVarSet = ∅
right✝ : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet ∪ (sub σ τ psi).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet ∪ (sub σ τ psi).metaVarSet = ∅
Tactic:
simp only [Finset.union_eq_empty]
State after:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅ ∧ (sub σ τ psi).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅ ∧ (sub σ τ psi).metaVarSet = ∅
Tactic:
constructor
State after:
case left
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅

case right
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ psi).metaVarSet = ∅

State before:
case left
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Tactic:
exact phi_ih h1_left
State after:
no goals

State before:
case right
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ psi).metaVarSet = ∅
Tactic:
exact psi_ih h1_right
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : (forall_ x phi).metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet at h1
State after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅
Tactic:
unfold sub
State after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (forall_ (↑σ x) (sub σ τ phi)).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (forall_ (↑σ x) (sub σ τ phi)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
State after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅

State before:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Tactic:
exact phi_ih h1
State after:
no goals

State before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : (def_ X xs).metaVarSet = ∅
⊢ (sub σ τ (def_ X xs)).metaVarSet = ∅
Tactic:
rfl
State after:
no goals