internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (h1_P.iff_ h1_P')
Tactic:
apply IsDeduct.mp_ (Forall_ l (U.iff_ V))
Proof state after:
case h1.a.h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))

case h1.a.h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (Forall_ l (U.iff_ V))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply h1_ih
Proof state after:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
Tactic:
intro v a1
Proof state after:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a.h1
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
Tactic:
cases a1
Proof state after:
case h1.a.h1.a.h1.intro
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
left✝ : isFreeIn v U ∨ isFreeIn v V
right✝ : isBoundIn v h1_P
⊢ v ∈ l
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v ∈ l
Tactic:
case _ a1_left a1_right =>
  apply h2 v a1_left
  right
  apply a1_right
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v ∈ l
Tactic:
apply h2 v a1_left
Proof state after:
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v = h1_x ∨ isBoundIn v h1_P
Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v = h1_x ∨ isBoundIn v h1_P
Tactic:
right
Proof state after:
case h
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Theorem: FOL.NV.T_18_2
Proof state before:
case h
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Tactic:
apply a1_right
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct {Forall_ l (U.iff_ V)} (Forall_ l (U.iff_ V))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.h1.a.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ Forall_ l (U.iff_ V) ∈ {Forall_ l (U.iff_ V)}
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h1.a.a
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ Forall_ l (U.iff_ V) ∈ {Forall_ l (U.iff_ V)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ∀ H ∈ {Forall_ l (U.iff_ V)}, ¬isFreeIn h1_x H
Tactic:
intro H a1
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
H : Formula
a1 : H ∈ {Forall_ l (U.iff_ V)}
⊢ ¬isFreeIn h1_x H
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
H : Formula
a1 : H ∈ {Forall_ l (U.iff_ V)}
⊢ ¬isFreeIn h1_x H
Tactic:
simp at a1
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
H : Formula
a1 : H = Forall_ l (U.iff_ V)
⊢ ¬isFreeIn h1_x H
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
H : Formula
a1 : H = Forall_ l (U.iff_ V)
⊢ ¬isFreeIn h1_x H
Tactic:
subst a1
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬isFreeIn h1_x (Forall_ l (U.iff_ V))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬isFreeIn h1_x (Forall_ l (U.iff_ V))
Tactic:
simp only [Forall_isFreeIn]
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x (U.iff_ V))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x (U.iff_ V))
Tactic:
simp only [def_iff_]
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).and_ (V.imp_ U)))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).and_ (V.imp_ U)))
Tactic:
simp only [def_and_]
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).imp_ (V.imp_ U).not_).not_)
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).imp_ (V.imp_ U).not_).not_)
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ ((isFreeIn h1_x U ∨ isFreeIn h1_x V) ∨ isFreeIn h1_x V ∨ isFreeIn h1_x U))
Theorem: FOL.NV.T_18_2
Proof state before:
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ ((isFreeIn h1_x U ∨ isFreeIn h1_x V) ∨ isFreeIn h1_x V ∨ isFreeIn h1_x U))
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.T_18_2
Proof state before:
case exists_
U V P_U P_V : Formula
l : List VarName
x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (exists_ x✝ P_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((exists_ x✝ P_u✝).iff_ (exists_ x✝ P_v✝)))
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsProof (P_U.iff_ P_V)
Tactic:
apply
  IsDeduct.mp_
    (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ ((Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V)).imp_ (P_U.iff_ P_V))

case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ ((Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V)).imp_ (P_U.iff_ P_V))
Tactic:
apply T_18_2 U V P_U P_V ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList h1
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ ∀ (v : VarName),
    (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ ∀ (v : VarName),
    (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Tactic:
intro v a1
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Tactic:
simp
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ isBoundIn v P_U
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
simp only [isBoundIn_iff_mem_boundVarSet] at a1
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
⊢ (v ∈ U.freeVarSet ∨ v ∈ V.freeVarSet) ∧ v ∈ P_U.boundVarSet
Tactic:
exact a1
Proof state after:
no goals
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
Tactic:
simp only [Formula.Forall_]
Proof state after:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)
Theorem: FOL.NV.C_18_3
Proof state before:
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)
Tactic:
induction ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
Proof state after:
case a.nil
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])

case a.cons
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tail✝)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) (head✝ :: tail✝))
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])
Tactic:
case _ =>
  simp
  exact h2
Proof state after:
no goals
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) [])
Tactic:
simp
Proof state after:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (U.iff_ V)
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (U.iff_ V)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.C_18_3
Proof state before:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) (hd :: tl))
Tactic:
simp
Proof state after:
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ IsDeduct ∅ (forall_ hd (List.foldr forall_ (U.iff_ V) tl))