internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.ProofList.List.mem_cons_cons
Proof state before:
μ : Type ?u.897613
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
l : List α
a b x : α
hx : x ∈ l
⊢ x ∈ a :: b :: l
Tactic:
simp
Proof state after:
μ : Type ?u.897613
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
l : List α
a b x : α
hx : x ∈ l
⊢ x = a ∨ x = b ∨ x ∈ l
Theorem: LO.FirstOrder.Derivation.ProofList.List.mem_cons_cons
Proof state before:
μ : Type ?u.897613
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
l : List α
a b x : α
hx : x ∈ l
⊢ x = a ∨ x = b ∨ x ∈ l
Tactic:
exact Or.inr (Or.inr $ hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.Finset.mem_cons_cons
Proof state before:
μ : Type ?u.902623
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ s ⊆ insert a (insert b s)
Tactic:
intro x hx
Proof state after:
μ : Type ?u.902623
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b x : α
hx : x ∈ s
⊢ x ∈ insert a (insert b s)
Theorem: LO.FirstOrder.Derivation.ProofList.Finset.mem_cons_cons
Proof state before:
μ : Type ?u.902623
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b x : α
hx : x ∈ s
⊢ x ∈ insert a (insert b s)
Tactic:
simp
Proof state after:
μ : Type ?u.902623
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b x : α
hx : x ∈ s
⊢ x = a ∨ x = b ∨ x ∈ s
Theorem: LO.FirstOrder.Derivation.ProofList.Finset.mem_cons_cons
Proof state before:
μ : Type ?u.902623
L : Language
inst✝⁷ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁶ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁵ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Func
inst✝² : UniformlyPrimcodable L.Rel
inst✝¹ : Primcodable μ
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b x : α
hx : x ∈ s
⊢ x = a ∨ x = b ∨ x ∈ s
Tactic:
exact Or.inr (Or.inr $ hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.Finset.toList_subset_toList
Proof state before:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ s₁.toList ⊆ s₂.toList ↔ s₁ ⊆ s₂
Tactic:
simp[List.subset_def]
Proof state after:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ (∀ {a : α}, a ∈ s₁ → a ∈ s₂) ↔ s₁ ⊆ s₂
Theorem: LO.FirstOrder.Derivation.ProofList.Finset.toList_subset_toList
Proof state before:
μ : Type ?u.904427
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Type u_1
s₁ s₂ : Finset α
⊢ (∀ {a : α}, a ∈ s₁ → a ∈ s₂) ↔ s₁ ⊆ s₂
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
property✝ : CutFree (axL Γ r v)
⊢ (ofDerivation ⟨axL Γ r v, property✝⟩).isProper = true
Tactic:
simp[ofDerivation, isProper]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
property✝ : CutFree (verum Γ)
⊢ (ofDerivation ⟨verum Γ, property✝⟩).isProper = true
Tactic:
simp[ofDerivation, isProper]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H : CutFree (bp.and bq)
⊢ (ofDerivation ⟨bp.and bq, H⟩).isProper = true
Tactic:
have H : CutFree bp ∧ CutFree bq := by simpa [CutFree] using H
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp.and bq, H✝⟩).isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp.and bq, H✝⟩).isProper = true
Tactic:
simp[ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ isProper
      ((Code.and p q, p ⋏ q :: Γ) ::
        (Code.wk (p :: Γ), p :: p ⋏ q :: Γ) ::
          (Code.wk (q :: Γ), q :: p ⋏ q :: Γ) :: (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩)) =
    true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ isProper
      ((Code.and p q, p ⋏ q :: Γ) ::
        (Code.wk (p :: Γ), p :: p ⋏ q :: Γ) ::
          (Code.wk (q :: Γ), q :: p ⋏ q :: Γ) :: (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩)) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩).isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H✝ : CutFree (bp.and bq)
H : CutFree bp ∧ CutFree bq
⊢ (ofDerivation ⟨bp, ⋯⟩ ++ ofDerivation ⟨bq, ⋯⟩).isProper = true
Tactic:
exact isProper_append (isProper_ofDerivation ⟨bp, H.1⟩) (isProper_ofDerivation ⟨bq, H.2⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
bp : Derivation (p :: Γ)
bq : Derivation (q :: Γ)
H : CutFree (bp.and bq)
⊢ CutFree bp ∧ CutFree bq
Tactic:
simpa [CutFree] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b.or, H⟩).isProper = true
Tactic:
simp[ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ isProper ((Code.or p q, p ⋎ q :: Γ) :: (Code.wk (p :: q :: Γ), p :: q :: p ⋎ q :: Γ) :: ofDerivation ⟨b, ⋯⟩) = true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ isProper ((Code.or p q, p ⋎ q :: Γ) :: (Code.wk (p :: q :: Γ), p :: q :: p ⋎ q :: Γ) :: ofDerivation ⟨b, ⋯⟩) = true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧ Γ ⊆ p :: q :: p ⋎ q :: Γ
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧ Γ ⊆ p :: q :: p ⋎ q :: Γ
Tactic:
exact ⟨isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩, by simp[List.subset_def]; intro x hx; simp[hx]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ CutFree b
Tactic:
simpa[CutFree] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ Γ ⊆ p :: q :: p ⋎ q :: Γ
Tactic:
simp[List.subset_def]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ ∀ {a : SyntacticFormula L}, a ∈ Γ → a = p ∨ a = q ∨ a = p ⋎ q ∨ a ∈ Γ
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
⊢ ∀ {a : SyntacticFormula L}, a ∈ Γ → a = p ∨ a = q ∨ a = p ⋎ q ∨ a ∈ Γ
Tactic:
intro x hx
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
x : SyntacticFormula L
hx : x ∈ Γ
⊢ x = p ∨ x = q ∨ x = p ⋎ q ∨ x ∈ Γ
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p q : SyntacticFormula L
b : Derivation (p :: q :: Γ)
H : CutFree b.or
x : SyntacticFormula L
hx : x ∈ Γ
⊢ x = p ∨ x = q ∨ x = p ⋎ q ∨ x ∈ Γ
Tactic:
simp[hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b.all, H⟩).isProper = true
Tactic:
simp[ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ isProper
      ((Code.all p, (∀' p) :: Γ) ::
        (Code.wk ((Rew.hom Rew.free) p :: shifts Γ),
            (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ) ::
          ofDerivation ⟨b, ⋯⟩) =
    true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ isProper
      ((Code.all p, (∀' p) :: Γ) ::
        (Code.wk ((Rew.hom Rew.free) p :: shifts Γ),
            (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ) ::
          ofDerivation ⟨b, ⋯⟩) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧
    shifts Γ ⊆ (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true ∧
    shifts Γ ⊆ (Rew.hom Rew.free) p :: (∀' (Rew.hom ⇑) p) :: List.map (⇑(Rew.hom ⇑)) Γ
Tactic:
exact ⟨isProper_ofDerivation ⟨b, by simpa[CutFree] using H⟩, List.subset_cons_of_subset _ $ List.subset_cons_of_subset _ $ by simp[shifts]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ CutFree b
Tactic:
simpa[CutFree] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
b : Derivation ((Rew.hom Rew.free) p :: shifts Γ)
H : CutFree b.all
⊢ shifts Γ ⊆ List.map (⇑(Rew.hom ⇑)) Γ
Tactic:
simp[shifts]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ (ofDerivation ⟨ex t b, H⟩).isProper = true
Tactic:
simp[ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ isProper
      ((Code.ex p t, (∃' p) :: Γ) :: (Code.wk ([→ t].hom p :: Γ), [→ t].hom p :: (∃' p) :: Γ) :: ofDerivation ⟨b, ⋯⟩) =
    true
Theorem: LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation
Proof state before:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ isProper
      ((Code.ex p t, (∃' p) :: Γ) :: (Code.wk ([→ t].hom p :: Γ), [→ t].hom p :: (∃' p) :: Γ) :: ofDerivation ⟨b, ⋯⟩) =
    true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation]
Proof state after:
μ : Type ?u.910235
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
Γ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true