internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) xs) =
    BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) xs))
⊢ v ∈ xs → u ∉ binders
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp at h2
  simp only [List.map_eq_map_iff] at h2
  intro a1
  specialize h2 v a1
  simp at h2
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
case eq_ x y =>
  simp at h2
  cases h2
  case intro h2_left h2_right =>
    intros a1
    cases a1
    case inl a1 =>
      subst a1
      simp at h2_left
      tauto
    case inr a1 =>
      subst a1
      simp at h2_right
      tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : (toIsBoundAux binders phi).not_ = (toIsBoundAux binders (fastReplaceFree v u phi)).not_
⊢ fastAdmitsAux v u binders phi
Tactic:
case not_ phi phi_ih =>
  simp at h2
  exact phi_ih binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u psi))
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp at h2
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (fastReplaceFree v u (def_ a✝¹ a✝))
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [fastReplaceFree] at h2
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
Tactic:
simp only [toIsBoundAux] at h2
Proof state after:
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) xs) =
    BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) xs))
⊢ v ∈ xs → u ∉ binders
Tactic:
simp at h2
Proof state after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  List.map (fun v => decide (v ∈ binders)) xs =
    List.map ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) xs
⊢ v ∈ xs → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  List.map (fun v => decide (v ∈ binders)) xs =
    List.map ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) xs
⊢ v ∈ xs → u ∉ binders
Tactic:
simp only [List.map_eq_map_iff] at h2
Proof state after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
⊢ v ∈ xs → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
⊢ v ∈ xs → u ∉ binders
Tactic:
intro a1
Proof state after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
a1 : v ∈ xs
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x
a1 : v ∈ xs
⊢ u ∉ binders
Tactic:
specialize h2 v a1
Proof state after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : decide (v ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) v
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : decide (v ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) v
⊢ u ∉ binders
Tactic:
simp at h2
Proof state after:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v ∈ xs
h2 : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
simp at h2
Proof state after:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)
⊢ v = x ∨ v = y → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
cases h2
Proof state after:
case intro
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
left✝ : x ∈ binders ↔ (if v = x then u else x) ∈ binders
right✝ : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
case intro h2_left h2_right =>
  intros a1
  cases a1
  case inl a1 =>
    subst a1
    simp at h2_left
    tauto
  case inr a1 =>
    subst a1
    simp at h2_right
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
Tactic:
intros a1
Proof state after:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x ∨ v = y
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x ∨ v = y
⊢ u ∉ binders
Tactic:
cases a1
Proof state after:
case inl
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h✝ : v = x
⊢ u ∉ binders

case inr
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h✝ : v = y
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x
⊢ u ∉ binders
Tactic:
case inl a1 =>
  subst a1
  simp at h2_left
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = y
⊢ u ∉ binders
Tactic:
case inr a1 =>
  subst a1
  simp at h2_right
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = x
⊢ u ∉ binders
Tactic:
subst a1
Proof state after:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Tactic:
simp at h2_left
Proof state after:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
h2_left : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
a1 : v = y
⊢ u ∉ binders
Tactic:
subst a1
Proof state after:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
Tactic:
simp at h2_right
Proof state after:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : (toIsBoundAux binders phi).not_ = (toIsBoundAux binders (fastReplaceFree v u phi)).not_
⊢ fastAdmitsAux v u binders phi
Tactic:
simp at h2
Proof state after:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
⊢ fastAdmitsAux v u binders phi
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
⊢ fastAdmitsAux v u binders phi
Tactic:
exact phi_ih binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u psi))
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
simp at h2
Proof state after:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) ∧
    toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi) → fastAdmitsAux v u binders psi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) ∧
    toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
⊢ fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
split_ifs at h2
Proof state after:
case pos
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h✝ : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi

case neg
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h✝ : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
case pos c1 =>
  left
  exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
left
Proof state after:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : v = x
h2 : BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) = toIsBoundAux binders (exists_ x phi)
⊢ v = x
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
right
Proof state after:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Theorem: FOL.NV.Sub.Var.One.Rec.free_and_bound_unchanged_imp_fastAdmitsAux
Proof state before:
case h
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ fastAdmitsAux v u (binders ∪ {x}) phi
Tactic:
apply phi_ih
Proof state after:
case h.h1
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∪ {x}

case h.h2
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
h2 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)