internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.evalPrime_prime
Proof state before:
F : Formula
V : VarBoolAssignment
h1 : F.IsPrime
⊢ evalPrime V F = (V F = true)
Tactic:
induction F
Proof state after:
case pred_const_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_const_ a✝¹ a✝) = (V (pred_const_ a✝¹ a✝) = true)

case pred_var_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_var_ a✝¹ a✝) = (V (pred_var_ a✝¹ a✝) = true)

case eq_
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).IsPrime
⊢ evalPrime V (eq_ a✝¹ a✝) = (V (eq_ a✝¹ a✝) = true)

case true_
V : VarBoolAssignment
h1 : true_.IsPrime
⊢ evalPrime V true_ = (V true_ = true)

case false_
V : VarBoolAssignment
h1 : false_.IsPrime
⊢ evalPrime V false_ = (V false_ = true)

case not_
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : a✝.not_.IsPrime
⊢ evalPrime V a✝.not_ = (V a✝.not_ = true)

case imp_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.imp_ a✝).IsPrime
⊢ evalPrime V (a✝¹.imp_ a✝) = (V (a✝¹.imp_ a✝) = true)

case and_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.and_ a✝).IsPrime
⊢ evalPrime V (a✝¹.and_ a✝) = (V (a✝¹.and_ a✝) = true)

case or_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.or_ a✝).IsPrime
⊢ evalPrime V (a✝¹.or_ a✝) = (V (a✝¹.or_ a✝) = true)

case iff_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)

case forall_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (forall_ a✝¹ a✝).IsPrime
⊢ evalPrime V (forall_ a✝¹ a✝) = (V (forall_ a✝¹ a✝) = true)

case exists_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (exists_ a✝¹ a✝).IsPrime
⊢ evalPrime V (exists_ a✝¹ a✝) = (V (exists_ a✝¹ a✝) = true)

case def_
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)
Theorem: FOL.NV.evalPrime_prime
Proof state before:
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)
Tactic:
case true_ | false_ | not_ | imp_ | and_ | or_ | iff_ =>
  simp only [Formula.IsPrime] at h1
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_prime
Proof state before:
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_prime
Proof state before:
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)
Tactic:
simp only [Formula.IsPrime] at h1
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_prime
Proof state before:
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  simp
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_
Tactic:
case true_ | false_ =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V (substPrime σ (phi.iff_ psi)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (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 only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
simp only [Formula.substPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ decide (evalPrime V (σ (def_ a✝¹ a✝))) = true
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ decide (evalPrime V (σ (def_ a✝¹ a✝))) = true
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
simp only [Formula.substPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi).not_ ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi).not_ ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
simp only [Formula.evalPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ ¬evalPrime V (substPrime σ phi) ↔ ¬evalPrime (fun H => decide (evalPrime V (σ H))) phi
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ ¬evalPrime V (substPrime σ phi) ↔ ¬evalPrime (fun H => decide (evalPrime V (σ H))) phi
Tactic:
congr! 1
Proof state after:
no goals
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V (substPrime σ (phi.iff_ psi)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Tactic:
simp only [Formula.substPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V ((substPrime σ phi).iff_ (substPrime σ psi)) ↔
    evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V ((substPrime σ phi).iff_ (substPrime σ psi)) ↔
    evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Tactic:
simp only [Formula.evalPrime]
Proof state after:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ (evalPrime V (substPrime σ phi) ↔ evalPrime V (substPrime σ psi)) ↔
    (evalPrime (fun H => decide (evalPrime V (σ H))) phi ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi)
Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime
Proof state before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ (evalPrime V (substPrime σ phi) ↔ evalPrime V (substPrime σ psi)) ↔
    (evalPrime (fun H => decide (evalPrime V (σ H))) phi ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi)
Tactic:
congr! 1
Proof state after:
no goals
Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime
Proof state before:
P : Formula
h1 : P.IsTautoPrime
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h1
Proof state after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime
Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime
Proof state before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ (substPrime σ P).IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime]
Proof state after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (substPrime σ P)
Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime
Proof state before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V (substPrime σ P)
Tactic:
intro V
Proof state after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ P)
Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime
Proof state before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ P)
Tactic:
simp only [evalPrime_substPrime_eq_evalPrime_evalPrime P σ V]
Proof state after:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime (fun H => decide (evalPrime V (σ H))) P
Theorem: FOL.NV.isTautoPrime_imp_isTautoPrime_substPrime
Proof state before:
P : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V P
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime (fun H => decide (evalPrime V (σ H))) P
Tactic:
apply h1
Proof state after:
no goals
Theorem: FOL.NV.T_13_5
Proof state before:
P : Formula
⊢ IsProof (P.imp_ P)
Tactic:
simp only [IsProof]
Proof state after:
P : Formula
⊢ IsDeduct ∅ (P.imp_ P)
Theorem: FOL.NV.T_13_5
Proof state before:
P : Formula
⊢ IsDeduct ∅ (P.imp_ P)
Tactic:
apply IsDeduct.mp_ (P.imp_ (P.imp_ P))
Proof state after:
case a
P : Formula
⊢ IsDeduct ∅ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P))

case a
P : Formula
⊢ IsDeduct ∅ (P.imp_ (P.imp_ P))
Theorem: FOL.NV.T_13_5
Proof state before:
case a
P : Formula
⊢ IsDeduct ∅ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P))
Tactic:
apply IsDeduct.mp_ (P.imp_ ((P.imp_ P).imp_ P))
Proof state after:
case a.a
P : Formula
⊢ IsDeduct ∅ ((P.imp_ ((P.imp_ P).imp_ P)).imp_ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P)))

case a.a
P : Formula
⊢ IsDeduct ∅ (P.imp_ ((P.imp_ P).imp_ P))
Theorem: FOL.NV.T_13_5
Proof state before:
case a.a
P : Formula
⊢ IsDeduct ∅ ((P.imp_ ((P.imp_ P).imp_ P)).imp_ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
P : Formula
⊢ IsAxiom ((P.imp_ ((P.imp_ P).imp_ P)).imp_ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P)))
Theorem: FOL.NV.T_13_5
Proof state before:
case a.a.a
P : Formula
⊢ IsAxiom ((P.imp_ ((P.imp_ P).imp_ P)).imp_ ((P.imp_ (P.imp_ P)).imp_ (P.imp_ P)))
Tactic:
exact IsAxiom.prop_2_ P (P.imp_ P) P
Proof state after:
no goals
Theorem: FOL.NV.T_13_5
Proof state before:
case a.a
P : Formula
⊢ IsDeduct ∅ (P.imp_ ((P.imp_ P).imp_ P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
P : Formula
⊢ IsAxiom (P.imp_ ((P.imp_ P).imp_ P))
Theorem: FOL.NV.T_13_5
Proof state before:
case a.a.a
P : Formula
⊢ IsAxiom (P.imp_ ((P.imp_ P).imp_ P))
Tactic:
exact IsAxiom.prop_1_ P (P.imp_ P)
Proof state after:
no goals
Theorem: FOL.NV.T_13_5
Proof state before:
case a
P : Formula
⊢ IsDeduct ∅ (P.imp_ (P.imp_ P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P : Formula
⊢ IsAxiom (P.imp_ (P.imp_ P))
Theorem: FOL.NV.T_13_5
Proof state before:
case a.a
P : Formula
⊢ IsAxiom (P.imp_ (P.imp_ P))
Tactic:
exact IsAxiom.prop_1_ P P
Proof state after:
no goals
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
P Q : Formula
⊢ IsProof (P.not_.imp_ (P.imp_ Q))
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ (Q.not_.imp_ P.not_))
Proof state after:
case a
P Q : Formula
⊢ IsDeduct ∅ ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q)))

case a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a
P Q : Formula
⊢ IsDeduct ∅ ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q)))
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))
Proof state after:
case a.a
P Q : Formula
⊢ IsDeduct ∅
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))

case a.a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a
P Q : Formula
⊢ IsDeduct ∅
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a
P Q : Formula
⊢ IsAxiom
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a.a
P Q : Formula
⊢ IsAxiom
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
Tactic:
apply IsAxiom.prop_2_
Proof state after:
no goals
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))
Tactic:
apply IsDeduct.mp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Proof state after:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))

case a.a.a
P Q : Formula
⊢ IsDeduct ∅ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a.a
P Q : Formula
⊢ IsAxiom (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a.a.a
P Q : Formula
⊢ IsAxiom (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
Tactic:
apply IsAxiom.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))
Theorem: FOL.NV.T_13_6_no_deduct
Proof state before:
case a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsAxiom.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) F
Tactic:
intro Γ
Proof state after:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
Γ : Set Formula
⊢ IsDeduct (Δ ∪ Γ) F
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
Γ : Set Formula
⊢ IsDeduct (Δ ∪ Γ) F
Tactic:
induction h1
Proof state after:
case axiom_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct (Δ ∪ Γ) phi✝

case assume_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) phi✝

case mp_
F : Formula
Δ Γ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct (Δ ∪ Γ) (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct (Δ ∪ Γ) phi✝
⊢ IsDeduct (Δ ∪ Γ) psi✝
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
case assume_ h1_phi h1_1 =>
  apply IsDeduct.assume_
  simp
  left
  exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Theorem: FOL.NV.T_14_10
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
apply IsDeduct.assume_
Proof state after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∪ Γ
Theorem: FOL.NV.T_14_10
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∪ Γ
Tactic:
simp
Proof state after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∨ h1_phi ∈ Γ
Theorem: FOL.NV.T_14_10
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∨ h1_phi ∈ Γ
Tactic:
left
Proof state after:
case a.h
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Theorem: FOL.NV.T_14_10
Proof state before:
case a.h
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_psi
Tactic:
apply IsDeduct.mp_ h1_phi
Proof state after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)

case a
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Theorem: FOL.NV.T_14_10
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
Tactic:
exact h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.T_14_10
Proof state before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
exact h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.T_14_10_comm
Proof state before:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Γ ∪ Δ) Q
Tactic:
simp only [Set.union_comm]
Proof state after:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) Q
Theorem: FOL.NV.T_14_10_comm
Proof state before:
Q : Formula
Δ : Set Formula
h1 : IsDeduct Δ Q
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) Q
Tactic:
exact T_14_10 Q Δ h1
Proof state after:
no goals
Theorem: FOL.NV.C_14_11
Proof state before:
P : Formula
h1 : IsProof P
⊢ ∀ (Δ : Set Formula), IsDeduct Δ P
Tactic:
intro Δ
Proof state after:
P : Formula
h1 : IsProof P
Δ : Set Formula
⊢ IsDeduct Δ P
Theorem: FOL.NV.C_14_11
Proof state before:
P : Formula
h1 : IsProof P
Δ : Set Formula
⊢ IsDeduct Δ P
Tactic:
obtain s1 := T_14_10 P ∅ h1 Δ
Proof state after:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct (∅ ∪ Δ) P
⊢ IsDeduct Δ P
Theorem: FOL.NV.C_14_11
Proof state before:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct (∅ ∪ Δ) P
⊢ IsDeduct Δ P
Tactic:
simp at s1
Proof state after:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Theorem: FOL.NV.C_14_11
Proof state before:
P : Formula
h1 : IsProof P
Δ : Set Formula
s1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact s1
Proof state after:
no goals