Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar (FOL/NV/Sub/Prop/All/Rec/Sub.lean)

State before:
F : Formula
τ : PredName → PredName
h1 : F.predVarSet = ∅
⊢ sub τ F = F
Tactic:
induction F
State after:
case pred_const_
τ : PredName → PredName
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
τ : PredName → PredName
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
τ : PredName → PredName
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
τ : PredName → PredName
h1 : true_.predVarSet = ∅
⊢ sub τ true_ = true_

case false_
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_

case not_
τ : PredName → PredName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : a✝.not_.predVarSet = ∅
⊢ sub τ a✝.not_ = a✝.not_

case imp_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.imp_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.and_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.or_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.iff_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
τ : PredName → PredName
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (forall_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
τ : PredName → PredName
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (exists_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
τ : PredName → PredName
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (def_ a✝¹ a✝) = def_ a✝¹ a✝

State before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ sub τ (pred_const_ X xs) = pred_const_ X xs
Tactic:
case pred_const_ X xs =>
  simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ sub τ (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:
τ : PredName → PredName
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ sub τ (eq_ x y) = eq_ x y
Tactic:
case eq_ x y =>
  simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_
Tactic:
case true_ | false_ =>
  simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [sub]
  congr!
  exact phi_ih h1
State after:
no goals

State before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ sub τ (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 [sub]
  congr!
  exact phi_ih h1
State after:
no goals

State before:
τ : PredName → PredName
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ sub τ (def_ X xs) = def_ X xs
Tactic:
case def_ X xs =>
  simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ sub τ (pred_const_ X xs) = pred_const_ X xs
Tactic:
simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp only [predVarSet] at h1
State after:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs

State before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp at h1
State after:
no goals

State before:
τ : PredName → PredName
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ sub τ (eq_ x y) = eq_ x y
Tactic:
simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_
Tactic:
simp only [sub]
State after:
no goals

State before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
simp only [predVarSet] at h1
State after:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_

State before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
simp only [sub]
State after:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ (sub τ phi).not_ = phi.not_

State before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ (sub τ phi).not_ = phi.not_
Tactic:
congr!
State after:
case h.e'_1
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi

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

State before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : (phi.iff_ psi).predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [predVarSet] at h1
State after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi

State before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [Finset.union_eq_empty] at h1
State after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi

State before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
cases h1
State after:
case intro
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
left✝ : phi.predVarSet = ∅
right✝ : psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi

State before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [sub]
State after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (sub τ phi).iff_ (sub τ psi) = phi.iff_ psi

State before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (sub τ phi).iff_ (sub τ psi) = phi.iff_ psi
Tactic:
congr!
State after:
case h.e'_1
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ phi = phi

case h.e'_2
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ psi = psi

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

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

State before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Tactic:
simp only [predVarSet] at h1
State after:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi

State before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Tactic:
simp only [sub]
State after:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (sub τ phi) = exists_ x phi

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

State before:
case h.e'_2
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi
Tactic:
exact phi_ih h1
State after:
no goals

State before:
τ : PredName → PredName
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ sub τ (def_ X xs) = def_ X xs
Tactic:
simp only [sub]
State after:
no goals