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

State before:
F : Formula
σ : Instantiation
τ τ' : MetaInstantiation
h1 : F.metaVarSet = ∅
⊢ sub σ τ F = sub σ τ' F
Tactic:
induction F
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✝)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)

State before:
σ : Instantiation
τ τ' : MetaInstantiation
X : MetaVarName
h1 : {X} = ∅
⊢ sub σ τ (meta_var_ X) = sub σ τ' (meta_var_ X)
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) = sub σ τ' (pred_ X xs)
Tactic:
rfl
State after:
no goals

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

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

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
State after:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_

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
State after:
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ (sub σ τ phi).not_ = (sub σ τ' phi).not_

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
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

State before:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Tactic:
exact phi_ih h1
State after:
no goals

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

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

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

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

State before:
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
Tactic:
congr! 1
State after:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi

case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ psi = sub σ τ' psi

State before:
case h.e'_1
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
Tactic:
exact phi_ih h1_left
State after:
no goals

State before:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ psi = sub σ τ' psi
Tactic:
exact psi_ih h1_right
State after:
no goals

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:
unfold Formula.metaVarSet at h1
State after:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ (forall_ x phi) = sub σ τ' (forall_ x phi)

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

State before:
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ forall_ (↑σ x) (sub σ τ phi) = forall_ (↑σ x) (sub σ τ' phi)
Tactic:
congr! 1
State after:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi

State before:
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
x : VarName
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi = sub σ τ' phi
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) = sub σ τ' (def_ X xs)
Tactic:
rfl
State after:
no goals