Theorem: FOL.NV.Sub.Pred.One.Rec.replace_no_predVar (FOL/NV/Sub/Pred/One/Rec/Sub.lean)

State before:
P : PredName
zs : List VarName
H F : Formula
h1 : F.predVarSet = ∅
⊢ replace P zs H F = F
Tactic:
induction F
State after:
case pred_const_
P : PredName
zs : List VarName
H : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
P : PredName
zs : List VarName
H : Formula
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
P : PredName
zs : List VarName
H : Formula
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
P : PredName
zs : List VarName
H : Formula
h1 : true_.predVarSet = ∅
⊢ replace P zs H true_ = true_

case false_
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_

case not_
P : PredName
zs : List VarName
H a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : a✝.not_.predVarSet = ∅
⊢ replace P zs H a✝.not_ = a✝.not_

case imp_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.imp_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.and_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.or_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
P : PredName
zs : List VarName
H a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → replace P zs H a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (a✝¹.iff_ a✝).predVarSet = ∅
⊢ replace P zs H (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
P : PredName
zs : List VarName
H : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (forall_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
P : PredName
zs : List VarName
H : Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → replace P zs H a✝ = a✝
h1 : (exists_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
P : PredName
zs : List VarName
H : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).predVarSet = ∅
⊢ replace P zs H (def_ a✝¹ a✝) = def_ a✝¹ a✝

State before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_const_ X xs) = pred_const_ X xs
Tactic:
case pred_const_ X xs =>
  simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
case pred_var_ X xs =>
  simp only [predVarSet] at h1
  simp at h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ replace P zs H (eq_ x y) = eq_ x y
Tactic:
case eq_ x y =>
  simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_
Tactic:
case true_ | false_ =>
  simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [replace]
  congr!
  exact phi_ih h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [replace]
  congr!
  exact phi_ih h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ replace P zs H (def_ X xs) = def_ X xs
Tactic:
case def_ X xs =>
  simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_const_ X xs) = pred_const_ X xs
Tactic:
simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp only [predVarSet] at h1
State after:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs

State before:
P : PredName
zs : List VarName
H : Formula
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ replace P zs H (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp at h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ replace P zs H (eq_ x y) = eq_ x y
Tactic:
simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
h1 : false_.predVarSet = ∅
⊢ replace P zs H false_ = false_
Tactic:
simp only [replace]
State after:
no goals

State before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
simp only [predVarSet] at h1
State after:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_

State before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
Tactic:
simp only [replace]
State after:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ (replace P zs H phi).not_ = phi.not_

State before:
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ (replace P zs H phi).not_ = phi.not_
Tactic:
congr!
State after:
case h.e'_1
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi

State before:
case h.e'_1
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : (phi.iff_ psi).predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [predVarSet] at h1
State after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi

State before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [Finset.union_eq_empty] at h1
State after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi

State before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
cases h1
State after:
case intro
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
left✝ : phi.predVarSet = ∅
right✝ : psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi

State before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [replace]
State after:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (replace P zs H phi).iff_ (replace P zs H psi) = phi.iff_ psi

State before:
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (replace P zs H phi).iff_ (replace P zs H psi) = phi.iff_ psi
Tactic:
congr!
State after:
case h.e'_1
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H phi = phi

case h.e'_2
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H psi = psi

State before:
case h.e'_1
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1_left
State after:
no goals

State before:
case h.e'_2
P : PredName
zs : List VarName
H phi psi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
psi_ih : psi.predVarSet = ∅ → replace P zs H psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H psi = psi
Tactic:
exact psi_ih h1_right
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
simp only [predVarSet] at h1
State after:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi

State before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H (exists_ x phi) = exists_ x phi
Tactic:
simp only [replace]
State after:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (replace P zs H phi) = exists_ x phi

State before:
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (replace P zs H phi) = exists_ x phi
Tactic:
congr!
State after:
case h.e'_2
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi

State before:
case h.e'_2
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
P : PredName
zs : List VarName
H : Formula
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ replace P zs H (def_ X xs) = def_ X xs
Tactic:
simp only [replace]
State after:
no goals