Theorem: FOL.NV.isFreeInInd_imp_isFreeIn (FOL/NV/Binders.lean)

State before:
v : VarName
F : Formula
h1 : isFreeInInd v F
⊢ isFreeIn v F
Tactic:
induction h1
State after:
case pred_const_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_const_ X✝ xs✝)

case pred_var_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_var_ X✝ xs✝)

case eq_
v : VarName
F : Formula
x✝ y✝ : VarName
a✝ : v = x✝ ∨ v = y✝
⊢ isFreeIn v (eq_ x✝ y✝)

case not_
v : VarName
F phi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v phi✝.not_

case imp_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case imp_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case and_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case and_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case or_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case or_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case iff_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case iff_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case forall_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (forall_ x✝ phi✝)

case exists_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (exists_ x✝ phi✝)

case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)

State before:
case pred_const_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_const_ X✝ xs✝)

case pred_var_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_var_ X✝ xs✝)

case eq_
v : VarName
F : Formula
x✝ y✝ : VarName
a✝ : v = x✝ ∨ v = y✝
⊢ isFreeIn v (eq_ x✝ y✝)

case not_
v : VarName
F phi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v phi✝.not_

case imp_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case imp_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case and_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case and_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case or_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case or_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case iff_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case iff_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case forall_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (forall_ x✝ phi✝)

case exists_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (exists_ x✝ phi✝)

case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
Tactic:
all_goals
  simp only [isFreeIn]
  tauto
State after:
no goals

State before:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
Tactic:
simp only [isFreeIn]
State after:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ v ∈ xs✝

State before:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ v ∈ xs✝
Tactic:
tauto
State after:
no goals