internlm/Lean-Github huggingface dataset:
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).imp_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).imp_ (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ psi)
Tactic:
congr! 1
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ x phi)) = sub (σ.comp σ') meta_var_ (forall_ x phi)
Tactic:
simp only [sub]
Proof state after:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑(σ.comp σ') x) (sub (σ.comp σ') meta_var_ phi)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑(σ.comp σ') x) (sub (σ.comp σ') meta_var_ phi)
Tactic:
unfold Instantiation.comp
Proof state after:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑⟨↑σ ∘ ↑σ', ⋯⟩ x) (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑⟨↑σ ∘ ↑σ', ⋯⟩ x) (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi)
Tactic:
congr! 1
Proof state after:
no goals
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ X xs)) = sub (σ.comp σ') meta_var_ (def_ X xs)
Tactic:
simp only [sub]
Proof state after:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑(σ.comp σ')) xs)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑(σ.comp σ')) xs)
Tactic:
unfold Instantiation.comp
Proof state after:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Theorem: MM0.sub_of_sub_is_sub_of_instantiation_comp
Proof state before:
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
F : Formula
σ : Instantiation
τ : MetaInstantiation
h1 : F.metaVarSet = ∅
⊢ (sub σ τ F).metaVarSet = ∅
Tactic:
induction F
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ (sub σ τ (eq_ x y)).metaVarSet = ∅
Tactic:
case eq_ x y =>
  rfl
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ (sub σ τ true_).metaVarSet = ∅
Tactic:
case true_ =>
  rfl
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet at h1
Proof state after:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ (sub σ τ (meta_var_ X)).metaVarSet = ∅
Tactic:
simp at h1
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : (pred_ X xs).metaVarSet = ∅
⊢ (sub σ τ (pred_ X xs)).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ (sub σ τ (eq_ x y)).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ (sub σ τ true_).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi.not_).metaVarSet = ∅
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_.metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_.metaVarSet = ∅
Tactic:
unfold Formula.metaVarSet
Proof state after:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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]
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof 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 = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ (forall_ x phi)).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (forall_ (↑σ x) (sub σ τ phi)).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
σ : Instantiation
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof 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
Proof state after:
no goals
Theorem: MM0.sub_preserves_empty_meta_var_set
Proof state before:
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : (def_ X xs).metaVarSet = ∅
⊢ (sub σ τ (def_ X xs)).metaVarSet = ∅
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
F : Formula
σ : Instantiation
τ τ' : MetaInstantiation
h1 : F.metaVarSet = ∅
⊢ sub σ τ F = sub σ τ' F
Tactic:
induction F
Proof state after:
case meta_var_
σ : Instantiation
τ τ' : MetaInstantiation
a✝ : MetaVarName
h1 : (meta_var_ a✝).metaVarSet = ∅
⊢ sub σ τ (meta_var_ a✝) = sub σ τ' (meta_var_ a✝)

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

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

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

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

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

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

case def_
σ : Instantiation
τ τ' : MetaInstantiation
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).metaVarSet = ∅
⊢ sub σ τ (def_ a✝¹ a✝) = sub σ τ' (def_ a✝¹ a✝)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold Formula.metaVarSet at h1
  simp at h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : PredName
xs : List VarName
h1 : (pred_ X xs).metaVarSet = ∅
⊢ sub σ τ (pred_ X xs) = sub σ τ' (pred_ X xs)
Tactic:
case pred_ X xs =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ sub σ τ (eq_ x y) = sub σ τ' (eq_ x y)
Tactic:
case eq_ x y =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ sub σ τ true_ = sub σ τ' true_
Tactic:
case true_ =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.not_.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold Formula.metaVarSet at h1
  unfold sub
  congr! 1
  exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : (forall_ x phi).metaVarSet = ∅
⊢ sub σ τ (forall_ x phi) = sub σ τ' (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  unfold Formula.metaVarSet at h1
  unfold sub
  congr! 1
  exact phi_ih h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : DefName
xs : List VarName
h1 : (def_ X xs).metaVarSet = ∅
⊢ sub σ τ (def_ X xs) = sub σ τ' (def_ X xs)
Tactic:
case def_ X xs =>
  rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : (meta_var_ X).metaVarSet = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)
Tactic:
unfold Formula.metaVarSet at h1
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)
Tactic:
simp at h1
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
X : PredName
xs : List VarName
h1 : (pred_ X xs).metaVarSet = ∅
⊢ sub σ τ (pred_ X xs) = sub σ τ' (pred_ X xs)
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
x y : VarName
h1 : (eq_ x y).metaVarSet = ∅
⊢ sub σ τ (eq_ x y) = sub σ τ' (eq_ x y)
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
h1 : true_.metaVarSet = ∅
⊢ sub σ τ true_ = sub σ τ' true_
Tactic:
rfl
Proof state after:
no goals
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.not_.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_
Tactic:
unfold Formula.metaVarSet at h1
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_
Tactic:
unfold sub
Proof state after:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_ = (sub σ τ' phi).not_
Theorem: MM0.no_meta_var_imp_meta_instantiation_irrelevance_in_sub
Proof state before:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_ = (sub σ τ' phi).not_
Tactic:
congr! 1
Proof state after:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi