Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_admitsAux (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
F : Formula
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t F
⊢ admitsAux t v binders (replaceFreeAux v t binders F)
Tactic:
induction F generalizing binders
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_const_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_var_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (pred_var_ a✝¹ a✝))

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬occursIn t (eq_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (eq_ a✝¹ a✝))

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
⊢ admitsAux t v binders (replaceFreeAux v t binders true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
⊢ admitsAux t v binders (replaceFreeAux v t binders false_)

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝.not_
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝.not_)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.imp_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.imp_ a✝))

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.and_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.and_ a✝))

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.or_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.or_ a✝))

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.iff_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.iff_ a✝))

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (forall_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (forall_ a✝¹ a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (exists_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (exists_ a✝¹ a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))

State before:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_const_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (pred_var_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (pred_var_ a✝¹ a✝))

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬occursIn t (eq_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (eq_ a✝¹ a✝))

case true_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t true_
⊢ admitsAux t v binders (replaceFreeAux v t binders true_)

case false_
v t : VarName
binders : Finset VarName
h1 : ¬occursIn t false_
⊢ admitsAux t v binders (replaceFreeAux v t binders false_)

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝.not_
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝.not_)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.imp_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.imp_ a✝))

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.and_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.and_ a✝))

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.or_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.or_ a✝))

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (a✝¹.iff_ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (a✝¹.iff_ a✝))

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (forall_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (forall_ a✝¹ a✝))

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t (exists_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (exists_ a✝¹ a✝))

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Tactic:
all_goals
  simp only [occursIn] at h1
  simp only [replaceFreeAux]
  simp only [admitsAux]
State after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝ ∧ t ∉ binders → v ∉ binders

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝ ∧ t ∉ binders → v ∉ binders

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ t = a✝)
⊢ ((t = if v = a✝¹ ∧ a✝¹ ∉ binders then t else a✝¹) ∨ t = if v = a✝ ∧ a✝ ∉ binders then t else a✝) ∧ t ∉ binders →
    v ∉ binders

case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝ ∧ t ∉ binders → v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs ∧ t ∉ binders → v ∉ binders
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x a1 a2 a3
  by_cases c1 : v = x ∧ x ∉ binders
  case pos =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case neg =>
    simp at c1
    specialize a2 c1
    subst a2
    contradiction
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1 : ¬(t = x ∨ t = y)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
case eq_ x y =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    intro a1
    split_ifs at a1
    case _ c1 c2 =>
      cases c1
      case intro c1_left c1_right =>
        subst c1_left
        exact c1_right
    case _ c1 c2 =>
      cases c1
      case intro c1_left c1_right =>
        subst c1_left
        exact c1_right
    case _ c1 c2 =>
      cases c2
      case intro c2_left c2_right =>
        subst c2_left
        exact c2_right
    case _ c1 c2 =>
      tauto
State after:
no goals

State before:
case not_
v t : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬occursIn t a✝
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝)

case imp_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case and_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case or_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case iff_
v t : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (binders : Finset VarName), ¬occursIn t a✝¹ → admitsAux t v binders (replaceFreeAux v t binders a✝¹)
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(occursIn t a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders a✝¹) ∧ admitsAux t v binders (replaceFreeAux v t binders a✝)

case forall_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)

case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)
Tactic:
all_goals
  tauto
State after:
no goals

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬occursIn t (def_ a✝¹ a✝)
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Tactic:
simp only [occursIn] at h1
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux t v binders (replaceFreeAux v t binders (def_ a✝¹ a✝))
Tactic:
simp only [replaceFreeAux]
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝))

State before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ admitsAux t v binders (def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝))
Tactic:
simp only [admitsAux]
State after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : t ∉ a✝
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝ ∧ t ∉ binders → v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs ∧ t ∉ binders → v ∉ binders
Tactic:
simp
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((v = x → x ∈ binders) → x = t) → t ∉ binders → v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((v = x → x ∈ binders) → x = t) → t ∉ binders → v ∉ binders
Tactic:
intro x a1 a2 a3
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
⊢ v ∉ binders
Tactic:
by_cases c1 : v = x ∧ x ∉ binders
State after:
case pos
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders

case neg
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders
Tactic:
case pos =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_right
State after:
no goals

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Tactic:
case neg =>
  simp at c1
  specialize a2 c1
  subst a2
  contradiction
State after:
no goals

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : v = x ∧ x ∉ binders
⊢ v ∉ binders
Tactic:
cases c1
State after:
case intro
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case intro c1_left c1_right =>
  subst c1_left
  exact c1_right
State after:
no goals

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
a3 : t ∉ binders
a1 : v ∈ xs
a2 : (v = v → v ∈ binders) → v = t
c1_right : v ∉ binders
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
a3 : t ∉ binders
a1 : v ∈ xs
a2 : (v = v → v ∈ binders) → v = t
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_right
State after:
no goals

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : ¬(v = x ∧ x ∉ binders)
⊢ v ∉ binders
Tactic:
simp at c1
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : v = x → x ∈ binders
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a2 : (v = x → x ∈ binders) → x = t
a3 : t ∉ binders
c1 : v = x → x ∈ binders
⊢ v ∉ binders
Tactic:
specialize a2 c1
State after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a3 : t ∉ binders
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders

State before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
a3 : t ∉ binders
c1 : v = x → x ∈ binders
a2 : x = t
⊢ v ∉ binders
Tactic:
subst a2
State after:
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
a3 : x ∉ binders
⊢ v ∉ binders

State before:
v : VarName
X : DefName
xs : List VarName
binders : Finset VarName
x : VarName
a1 : x ∈ xs
c1 : v = x → x ∈ binders
h1 : x ∉ xs
a3 : x ∉ binders
⊢ v ∉ binders
Tactic:
contradiction
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1 : ¬(t = x ∨ t = y)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
push_neg at h1
State after:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
cases h1
State after:
case intro
v t x y : VarName
binders : Finset VarName
left✝ : t ≠ x
right✝ : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
case intro h1_left h1_right =>
  intro a1
  split_ifs at a1
  case _ c1 c2 =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case _ c1 c2 =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case _ c1 c2 =>
    cases c2
    case intro c2_left c2_right =>
      subst c2_left
      exact c2_right
  case _ c1 c2 =>
    tauto
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
Tactic:
intro a1
State after:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
a1 : ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders
⊢ v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
a1 : ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
split_ifs at a1
State after:
case pos
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
h✝¹ : v = x ∧ x ∉ binders
h✝ : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders

case neg
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
h✝¹ : v = x ∧ x ∉ binders
h✝ : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders

case pos
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
h✝¹ : ¬(v = x ∧ x ∉ binders)
h✝ : v = y ∧ y ∉ binders
a1 : (t = x ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders

case neg
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
h✝¹ : ¬(v = x ∧ x ∉ binders)
h✝ : ¬(v = y ∧ y ∉ binders)
a1 : (t = x ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c1
  case intro c1_left c1_right =>
    subst c1_left
    exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : v = y ∧ y ∉ binders
a1 : (t = x ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  cases c2
  case intro c2_left c2_right =>
    subst c2_left
    exact c2_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = x ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
case _ c1 c2 =>
  tauto
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
cases c1
State after:
case intro
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case intro c1_left c1_right =>
  subst c1_left
  exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
State after:
v t y : VarName
binders : Finset VarName
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
h1_left : t ≠ v
c1_right : v ∉ binders
⊢ v ∉ binders

State before:
v t y : VarName
binders : Finset VarName
h1_right : t ≠ y
c2 : v = y ∧ y ∉ binders
a1 : (t = t ∨ t = t) ∧ t ∉ binders
h1_left : t ≠ v
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : v = x ∧ x ∉ binders
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
cases c1
State after:
case intro
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
left✝ : v = x
right✝ : x ∉ binders
⊢ v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
case intro c1_left c1_right =>
  subst c1_left
  exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
c1_left : v = x
c1_right : x ∉ binders
⊢ v ∉ binders
Tactic:
subst c1_left
State after:
v t y : VarName
binders : Finset VarName
h1_right : t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
h1_left : t ≠ v
c1_right : v ∉ binders
⊢ v ∉ binders

State before:
v t y : VarName
binders : Finset VarName
h1_right : t ≠ y
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = t ∨ t = y) ∧ t ∉ binders
h1_left : t ≠ v
c1_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c1_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : v = y ∧ y ∉ binders
a1 : (t = x ∨ t = t) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
cases c2
State after:
case intro
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
left✝ : v = y
right✝ : y ∉ binders
⊢ v ∉ binders

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
c2_left : v = y
c2_right : y ∉ binders
⊢ v ∉ binders
Tactic:
case intro c2_left c2_right =>
  subst c2_left
  exact c2_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
c2_left : v = y
c2_right : y ∉ binders
⊢ v ∉ binders
Tactic:
subst c2_left
State after:
v t x : VarName
binders : Finset VarName
h1_left : t ≠ x
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
h1_right : t ≠ v
c2_right : v ∉ binders
⊢ v ∉ binders

State before:
v t x : VarName
binders : Finset VarName
h1_left : t ≠ x
c1 : ¬(v = x ∧ x ∉ binders)
a1 : (t = x ∨ t = t) ∧ t ∉ binders
h1_right : t ≠ v
c2_right : v ∉ binders
⊢ v ∉ binders
Tactic:
exact c2_right
State after:
no goals

State before:
v t x y : VarName
binders : Finset VarName
h1_left : t ≠ x
h1_right : t ≠ y
c1 : ¬(v = x ∧ x ∉ binders)
c2 : ¬(v = y ∧ y ∉ binders)
a1 : (t = x ∨ t = y) ∧ t ∉ binders
⊢ v ∉ binders
Tactic:
tauto
State after:
no goals

State before:
case exists_
v t a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (binders : Finset VarName), ¬occursIn t a✝ → admitsAux t v binders (replaceFreeAux v t binders a✝)
binders : Finset VarName
h1 : ¬(t = a✝¹ ∨ occursIn t a✝)
⊢ admitsAux t v (binders ∪ {a✝¹}) (replaceFreeAux v t (binders ∪ {a✝¹}) a✝)
Tactic:
tauto
State after:
no goals