internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_is_proof
Proof state before:
case intro.hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
⊢ ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E F
Tactic:
intro psi V' a2
Proof state after:
case intro.hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Theorem: MM0.holds_is_proof
Proof state before:
case intro.hyp
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 :
  ∀ psi ∈ h1_Δ,
    ∀ (M : MetaValuation D),
      (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v) →
        (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F) →
          ∀ (V : Valuation D), Holds D I V M E (sub h1_σ h1_τ psi)
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ' → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ' → Holds D I V M E F
σ' : VarName → VarName
a1 : ↑h1_σ ∘ σ' = id ∧ σ' ∘ ↑h1_σ = id
s1 : IsMetaVarOrAllDefInEnv E h1_phi
V : Valuation D
psi : Formula
V' : Valuation D
a2 : psi ∈ h1_Δ
s2 : IsMetaVarOrAllDefInEnv E psi
s3 : Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
⊢ Holds D I V' (fun X' V' => Holds D I (V' ∘ σ') M E (h1_τ X')) E psi
Tactic:
exact s3
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi'
Tactic:
intro V
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ Holds D I V M E h1_phi'
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
⊢ Holds D I V M E h1_phi'
Tactic:
have s1 : Holds D I V M E h1_phi := h1_ih M nf hyp V
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi'
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi'
Tactic:
simp only [← holds_conv D I V M E h1_phi h1_phi' h2 h1_3]
Proof state after:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_phi' : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi'
h1_2 : IsProof E h1_Γ h1_Δ h1_phi
h1_3 : IsConv E h1_phi h1_phi'
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
V : Valuation D
s1 : Holds D I V M E h1_phi
⊢ Holds D I V M E h1_phi
Tactic:
exact s1
Proof state after:
no goals
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
x : Except ε α
f : α → Except ε β
a : β
⊢ x.bind f = ok a ↔ ∃ b, x = ok b ∧ f b = ok a
Tactic:
cases x
Proof state after:
case error
ε α β : Type
f : α → Except ε β
a : β
a✝ : ε
⊢ (error a✝).bind f = ok a ↔ ∃ b, error a✝ = ok b ∧ f b = ok a

case ok
ε α β : Type
f : α → Except ε β
a : β
a✝ : α
⊢ (ok a✝).bind f = ok a ↔ ∃ b, ok a✝ = ok b ∧ f b = ok a
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
case error x =>
  simp only [Except.bind]
  simp
Proof state after:
no goals
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
case ok x =>
  simp only [Except.bind]
  simp
Proof state after:
no goals
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
Proof state after:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a
Tactic:
simp
Proof state after:
no goals
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
Proof state after:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Theorem: Except.bind_eq_ok
Proof state before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_1
Proof state before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (fastReplaceFree v t P)
Tactic:
apply IsDeduct.mp_ (forall_ v P)
Proof state after:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ ((forall_ v P).imp_ (fastReplaceFree v t P))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (forall_ v P)
Theorem: FOL.NV.T_17_1
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ ((forall_ v P).imp_ (fastReplaceFree v t P))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsAxiom ((forall_ v P).imp_ (fastReplaceFree v t P))
Theorem: FOL.NV.T_17_1
Proof state before:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsAxiom ((forall_ v P).imp_ (fastReplaceFree v t P))
Tactic:
apply IsAxiom.pred_2_ v t P (fastReplaceFree v t P) h2
Proof state after:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ fastReplaceFree v t P = fastReplaceFree v t P
Theorem: FOL.NV.T_17_1
Proof state before:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ fastReplaceFree v t P = fastReplaceFree v t P
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_17_1
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (forall_ v P)
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.specId
Proof state before:
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ P
Tactic:
apply IsDeduct.mp_ (forall_ v P)
Proof state after:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ ((forall_ v P).imp_ P)

case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ (forall_ v P)
Theorem: FOL.NV.specId
Proof state before:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ ((forall_ v P).imp_ P)
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsAxiom ((forall_ v P).imp_ P)
Theorem: FOL.NV.specId
Proof state before:
case a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsAxiom ((forall_ v P).imp_ P)
Tactic:
apply IsAxiom.pred_2_ v v P
Proof state after:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastAdmits v v P

case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastReplaceFree v v P = P
Theorem: FOL.NV.specId
Proof state before:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastAdmits v v P
Tactic:
exact fastAdmits_self P v
Proof state after:
no goals
Theorem: FOL.NV.specId
Proof state before:
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastReplaceFree v v P = P
Tactic:
exact fastReplaceFree_self P v
Proof state after:
no goals
Theorem: FOL.NV.specId
Proof state before:
case a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsDeduct Δ (forall_ v P)
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_17_3
Proof state before:
P : Formula
v t : VarName
h1 : fastAdmits v t P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
simp only [fastAdmits] at h1
Proof state after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Theorem: FOL.NV.T_17_3
Proof state before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
simp only [def_exists_]
Proof state after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Theorem: FOL.NV.T_17_3
Proof state before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Tactic:
simp only [IsProof]
Proof state after:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Theorem: FOL.NV.T_17_3
Proof state before:
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_)
Tactic:
apply IsDeduct.mp_ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Proof state after:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅
    (((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_).imp_ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_))

case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Theorem: FOL.NV.T_17_3
Proof state before:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅
    (((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_).imp_ ((fastReplaceFree v t P).imp_ (forall_ v P.not_).not_))
Tactic:
SC
Proof state after:
no goals
Theorem: FOL.NV.T_17_3
Proof state before:
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsAxiom ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Theorem: FOL.NV.T_17_3
Proof state before:
case a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsAxiom ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
Tactic:
apply IsAxiom.pred_2_ v t
Proof state after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmits v t P.not_

case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastReplaceFree v t P.not_ = (fastReplaceFree v t P).not_
Theorem: FOL.NV.T_17_3
Proof state before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmits v t P.not_
Tactic:
simp only [fastAdmits]
Proof state after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P.not_
Theorem: FOL.NV.T_17_3
Proof state before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P.not_
Tactic:
simp only [fastAdmitsAux]
Proof state after:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P
Theorem: FOL.NV.T_17_3
Proof state before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_17_3
Proof state before:
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastReplaceFree v t P.not_ = (fastReplaceFree v t P).not_
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.T_17_4
Proof state before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ (exists_ v P)
Tactic:
apply IsDeduct.mp_ (fastReplaceFree v t P)
Proof state after:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ ((fastReplaceFree v t P).imp_ (exists_ v P))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ (fastReplaceFree v t P)
Theorem: FOL.NV.T_17_4
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
apply proof_imp_deduct
Proof state after:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Theorem: FOL.NV.T_17_4
Proof state before:
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
Tactic:
apply T_17_3
Proof state after:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ fastAdmits v t P
Theorem: FOL.NV.T_17_4
Proof state before:
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ fastAdmits v t P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_17_4
Proof state before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ (fastReplaceFree v t P)
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.existsIntroId
Proof state before:
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (exists_ v P)
Tactic:
apply T_17_4 P v v Δ
Proof state after:
case h1
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ fastAdmits v v P

case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)
Theorem: FOL.NV.existsIntroId
Proof state before:
case h1
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ fastAdmits v v P
Tactic:
exact fastAdmits_self P v
Proof state after:
no goals
Theorem: FOL.NV.existsIntroId
Proof state before:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)
Tactic:
simp only [fastReplaceFree_self]
Proof state after:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Theorem: FOL.NV.existsIntroId
Proof state before:
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.T_17_6
Proof state before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).imp_ (exists_ v P))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v P}) (exists_ v P)
Theorem: FOL.NV.T_17_6
Proof state before:
case h1
P : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v P}) (exists_ v P)
Tactic:
simp
Proof state after:
case h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (exists_ v P)
Theorem: FOL.NV.T_17_6
Proof state before:
case h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (exists_ v P)
Tactic:
apply existsIntroId
Proof state after:
case h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} P
Theorem: FOL.NV.T_17_6
Proof state before:
case h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} P
Tactic:
apply specId v
Proof state after:
case h1.h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (forall_ v P)
Theorem: FOL.NV.T_17_6
Proof state before:
case h1.h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (forall_ v P)
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.a
P : Formula
v : VarName
⊢ forall_ v P ∈ {forall_ v P}
Theorem: FOL.NV.T_17_6
Proof state before:
case h1.h1.h1.a
P : Formula
v : VarName
⊢ forall_ v P ∈ {forall_ v P}
Tactic:
simp
Proof state after:
no goals