internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
F : Formula
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders F = F
Tactic:
induction F generalizing binders
Proof state after:
case pred_const_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
v t : VarName
a✝¹ : PredName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
v t a✝¹ a✝ : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders true_ = true_

case false_
v t : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders false_ = false_

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

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

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

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

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

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

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

case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) = def_ X xs
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  simp only [List.map_eq_self_iff]
  simp
  intro x _ a2 a3
  subst a2
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) = eq_ x y
Tactic:
case eq_ x y =>
  simp
  constructor
  case left | right =>
    intro a1 a2
    subst a1
    contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).iff_ (replaceFreeAux v t binders psi) = phi.iff_ 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
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  apply phi_ih
  simp
  left
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = def_ a✝¹ a✝
Tactic:
simp only [replaceFreeAux]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) = def_ X xs
Tactic:
simp
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs = xs
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs = xs
Tactic:
simp only [List.map_eq_self_iff]
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, (if v = x ∧ x ∉ binders then t else x) = x
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, (if v = x ∧ x ∉ binders then t else x) = x
Tactic:
simp
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, v = x → x ∉ binders → t = x
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, v = x → x ∉ binders → t = x
Tactic:
intro x _ a2 a3
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
x : VarName
a✝ : x ∈ xs
a2 : v = x
a3 : x ∉ binders
⊢ t = x
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
x : VarName
a✝ : x ∈ xs
a2 : v = x
a3 : x ∉ binders
⊢ t = x
Tactic:
subst a2
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
a✝ : v ∈ xs
a3 : v ∉ binders
⊢ t = v
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
a✝ : v ∈ xs
a3 : v ∉ binders
⊢ t = v
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) = eq_ x y
Tactic:
simp
Proof state after:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)
Tactic:
constructor
Proof state after:
case left
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = x → x ∉ binders → t = x

case right
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y
Tactic:
case left | right =>
  intro a1 a2
  subst a1
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ v = y → y ∉ binders → t = y
Tactic:
intro a1 a2
Proof state after:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
a1 : v = y
a2 : y ∉ binders
⊢ t = y
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
a1 : v = y
a2 : y ∉ binders
⊢ t = y
Tactic:
subst a1
Proof state after:
v t x : VarName
binders : Finset VarName
h1 : v ∈ binders
a2 : v ∉ binders
⊢ t = v
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x : VarName
binders : Finset VarName
h1 : v ∈ binders
a2 : v ∉ binders
⊢ t = v
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).not_ = phi.not_
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ (replaceFreeAux v t binders phi).iff_ (replaceFreeAux v t binders psi) = phi.iff_ psi
Tactic:
simp
Proof state after:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders phi = phi ∧ replaceFreeAux v t binders psi = psi
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
psi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders psi = psi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t binders phi = phi ∧ replaceFreeAux v t binders psi = psi
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) = exists_ x phi
Tactic:
simp
Proof state after:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t (binders ∪ {x}) phi = phi
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ replaceFreeAux v t (binders ∪ {x}) phi = phi
Tactic:
apply phi_ih
Proof state after:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∪ {x}
Tactic:
simp
Proof state after:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∨ v = x
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
case h1
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders ∨ v = x
Tactic:
left
Proof state after:
case h1.h
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_mem_binders
Proof state before:
case h1.h
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∈ binders → replaceFreeAux v t binders phi = phi
binders : Finset VarName
h1 : v ∈ binders
⊢ v ∈ binders
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) =
    def_ X (List.map (fun x => if v = x then t else x) xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  congr!
  case _ x =>
    constructor
    case mp =>
      tauto
    case mpr =>
      intro a1
      subst a1
      tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) =
    eq_ (if v = x then t else x) (if v = y then t else y)
Tactic:
case eq_ x y =>
  congr!
  case _ | _ =>
    constructor
    case mp =>
      tauto
    case mpr =>
      intro a1
      subst a1
      tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
binders : Finset VarName
h1 : v ∉ binders
⊢ (replaceFreeAux v t binders phi).not_ = (fastReplaceFree v t phi).not_
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
psi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders psi = fastReplaceFree v t psi
binders : Finset VarName
h1 : v ∉ binders
⊢ (replaceFreeAux v t binders phi).iff_ (replaceFreeAux v t binders psi) =
    (fastReplaceFree v t phi).iff_ (fastReplaceFree v t 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
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
binders : Finset VarName
h1 : v ∉ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) =
    if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  split_ifs
  case pos c1 =>
    congr! 1
    apply replaceFreeAux_mem_binders
    simp
    right
    exact c1
  case neg c1 =>
    congr! 1
    apply phi_ih
    simp
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = fastReplaceFree v t (def_ a✝¹ a✝)
Tactic:
simp only [replaceFreeAux]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = fastReplaceFree v t (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = fastReplaceFree v t (def_ a✝¹ a✝)
Tactic:
simp only [fastReplaceFree]
Proof state after:
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) =
    def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝)
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) =
    def_ X (List.map (fun x => if v = x then t else x) xs)
Tactic:
congr!
Proof state after:
case h.e'_2.h.e'_3.h.h₁.a
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x✝ : VarName
⊢ v = x✝ ∧ x✝ ∉ binders ↔ v = x✝
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders ↔ v = x
Tactic:
case _ x =>
  constructor
  case mp =>
    tauto
  case mpr =>
    intro a1
    subst a1
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders ↔ v = x
Tactic:
constructor
Proof state after:
case mp
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders → v = x

case mpr
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x → v = x ∧ x ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders → v = x
Tactic:
case mp =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x → v = x ∧ x ∉ binders
Tactic:
case mpr =>
  intro a1
  subst a1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x ∧ x ∉ binders → v = x
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
⊢ v = x → v = x ∧ x ∉ binders
Tactic:
intro a1
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
a1 : v = x
⊢ v = x ∧ x ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
a1 : v = x
⊢ v = x ∧ x ∉ binders
Tactic:
subst a1
Proof state after:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = v ∧ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = v ∧ v ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) =
    eq_ (if v = x then t else x) (if v = y then t else y)
Tactic:
congr!
Proof state after:
case h.e'_1.h₁.a
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = x ∧ x ∉ binders ↔ v = x

case h.e'_2.h₁.a
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders ↔ v = y
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders ↔ v = y
Tactic:
case _ | _ =>
  constructor
  case mp =>
    tauto
  case mpr =>
    intro a1
    subst a1
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders ↔ v = y
Tactic:
constructor
Proof state after:
case mp
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders → v = y

case mpr
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y → v = y ∧ y ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders → v = y
Tactic:
case mp =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y → v = y ∧ y ∉ binders
Tactic:
case mpr =>
  intro a1
  subst a1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders → v = y
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y → v = y ∧ y ∉ binders
Tactic:
intro a1
Proof state after:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v = y
⊢ v = y ∧ y ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
a1 : v = y
⊢ v = y ∧ y ∉ binders
Tactic:
subst a1
Proof state after:
v t x : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = v ∧ v ∉ binders
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t x : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = v ∧ v ∉ binders
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.replaceFreeAux_eq_fastReplaceFree
Proof state before:
v t : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
binders : Finset VarName
h1 : v ∉ binders
⊢ (replaceFreeAux v t binders phi).not_ = (fastReplaceFree v t phi).not_
Tactic:
tauto
Proof state after:
no goals