internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_21_8
Proof state before:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct (∅ ∪ {eq_ r s}) ((forall_ x P_u).iff_ (forall_ x P_v))
Tactic:
simp
Proof state after:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x P_u).iff_ (forall_ x P_v))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x P_u).iff_ (forall_ x P_v))
Tactic:
apply IsDeduct.mp_ (forall_ x (P_u.iff_ P_v))
Proof state after:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (forall_ x (P_u.iff_ P_v))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply T_18_1
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (forall_ x (P_u.iff_ P_v))
Tactic:
apply IsDeduct.mp_ (eq_ r s)
Proof state after:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))

case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (eq_ r s)
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))
Tactic:
apply proof_imp_deduct
Proof state after:
case h1.a.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))
Tactic:
apply IsDeduct.mp_ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))
Proof state after:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v))).imp_ ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v))))

case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v))).imp_ ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v))))
Tactic:
apply T_19_TS_21_left
Proof state after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬isFreeIn x (eq_ r s)
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬isFreeIn x (eq_ r s)
Tactic:
simp only [isFreeIn]
Proof state after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬(x = r ∨ x = s)
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬(x = r ∨ x = s)
Tactic:
push_neg
Proof state after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r ∧ x ≠ s
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r ∧ x ≠ s
Tactic:
constructor
Proof state after:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r

case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ s
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r
Tactic:
simp only [ne_comm]
Proof state after:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ r ≠ x
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ r ≠ x
Tactic:
exact h2_left
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ s
Tactic:
simp only [ne_comm]
Proof state after:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ s ≠ x
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ s ≠ x
Tactic:
exact h3_left
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))
Tactic:
apply generalization
Proof state after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))

case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih h2_right h3_right
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Tactic:
intro H a1
Proof state after:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Tactic:
simp at a1
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (eq_ r s)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.a.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ eq_ r s ∈ {eq_ r s}
Theorem: FOL.NV.T_21_8
Proof state before:
case h1.a.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ eq_ r s ∈ {eq_ r s}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof state before:
case exists_
P_r P_s : Formula
r s x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfVarInFormula r s P_u✝ P_v✝
a_ih✝ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
h2 : ¬isBoundIn r (exists_ x✝ P_u✝)
h3 : ¬isBoundIn s (exists_ x✝ P_u✝)
⊢ IsProof ((eq_ r s).imp_ ((exists_ x✝ P_u✝).iff_ (exists_ x✝ P_v✝)))
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
F : Formula
τ : PredName → PredName
h1 : F.predVarSet = ∅
⊢ sub τ F = F
Tactic:
induction F
Proof state after:
case pred_const_
τ : PredName → PredName
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
τ : PredName → PredName
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
τ : PredName → PredName
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_
τ : PredName → PredName
h1 : true_.predVarSet = ∅
⊢ sub τ true_ = true_

case false_
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_

case not_
τ : PredName → PredName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : a✝.not_.predVarSet = ∅
⊢ sub τ a✝.not_ = a✝.not_

case imp_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.imp_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.and_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.or_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
τ : PredName → PredName
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.predVarSet = ∅ → sub τ a✝¹ = a✝¹
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (a✝¹.iff_ a✝).predVarSet = ∅
⊢ sub τ (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
τ : PredName → PredName
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (forall_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
τ : PredName → PredName
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.predVarSet = ∅ → sub τ a✝ = a✝
h1 : (exists_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
τ : PredName → PredName
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).predVarSet = ∅
⊢ sub τ (def_ a✝¹ a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ sub τ (pred_const_ X xs) = pred_const_ X xs
Tactic:
case pred_const_ X xs =>
  simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Tactic:
case pred_var_ X xs =>
  simp only [predVarSet] at h1
  simp at h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ sub τ (eq_ x y) = eq_ x y
Tactic:
case eq_ x y =>
  simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_
Tactic:
case true_ | false_ =>
  simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [sub]
  congr!
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [sub]
  congr!
  exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ sub τ (def_ X xs) = def_ X xs
Tactic:
case def_ X xs =>
  simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_const_ X xs).predVarSet = ∅
⊢ sub τ (pred_const_ X xs) = pred_const_ X xs
Tactic:
simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : (pred_var_ X xs).predVarSet = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp only [predVarSet] at h1
Proof state after:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : PredName
xs : List VarName
h1 : {(X, xs.length)} = ∅
⊢ sub τ (pred_var_ X xs) = pred_var_ X xs
Tactic:
simp at h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x y : VarName
h1 : (eq_ x y).predVarSet = ∅
⊢ sub τ (eq_ x y) = eq_ x y
Tactic:
simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
h1 : false_.predVarSet = ∅
⊢ sub τ false_ = false_
Tactic:
simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
simp only [predVarSet] at h1
Proof state after:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
Tactic:
simp only [sub]
Proof state after:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ (sub τ phi).not_ = phi.not_
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ (sub τ phi).not_ = phi.not_
Tactic:
congr!
Proof state after:
case h.e'_1
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
case h.e'_1
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : (phi.iff_ psi).predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [predVarSet] at h1
Proof state after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet ∪ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [Finset.union_eq_empty] at h1
Proof state after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1 : phi.predVarSet = ∅ ∧ psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
cases h1
Proof state after:
case intro
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
left✝ : phi.predVarSet = ∅
right✝ : psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi