internlm/Lean-Github huggingface dataset:
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 ⟨b, ⋯⟩).isProper = true
Tactic:
exact isProper_ofDerivation ⟨b, by 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 : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
b : Derivation ([→ t].hom p :: Γ)
H : CutFree (ex t b)
⊢ 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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b.wk ss, 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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ isProper ((Code.wk Γ, Γ') :: 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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ isProper ((Code.wk Γ, Γ') :: ofDerivation ⟨b, ⋯⟩) = true
Tactic:
simp[isProper, sequents_cons, List.mem_cons_cons, mem_ofDerivation, ss]
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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b, ⋯⟩).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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ (ofDerivation ⟨b, ⋯⟩).isProper = true
Tactic:
exact isProper_ofDerivation ⟨b, by 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 μ
Γ' Γ : Sequent L
b : Derivation Γ
ss : Γ ⊆ Γ'
H : CutFree (b.wk ss)
⊢ CutFree b
Tactic:
simpa[CutFree] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
μ : Type ?u.1106645
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 μ
Γ : Sequent L
⊢ Nonempty ( ⊢¹ Γ) → ∃ l, l.isProper = true ∧ Γ ∈ l.sequents
Tactic:
rintro h
Proof state after:
μ : Type ?u.1106645
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 μ
Γ : Sequent L
h : Nonempty ( ⊢¹ Γ)
⊢ ∃ l, l.isProper = true ∧ Γ ∈ l.sequents
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
μ : Type ?u.1106645
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 μ
Γ : Sequent L
h : Nonempty ( ⊢¹ Γ)
⊢ ∃ l, l.isProper = true ∧ Γ ∈ l.sequents
Tactic:
rcases iff_cut.mpr h with ⟨b⟩
Proof state after:
case intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
h : Nonempty ( ⊢¹ Γ)
b : { d // CutFree d }
⊢ ∃ l, l.isProper = true ∧ Γ ∈ l.sequents
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
case intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
h : Nonempty ( ⊢¹ Γ)
b : { d // CutFree d }
⊢ ∃ l, l.isProper = true ∧ Γ ∈ l.sequents
Tactic:
exact ⟨ofDerivation b, isProper_ofDerivation b, mem_ofDerivation b⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
μ : Type ?u.1106645
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 μ
Γ : Sequent L
⊢ (∃ l, l.isProper = true ∧ Γ ∈ l.sequents) → Nonempty ( ⊢¹ Γ)
Tactic:
rintro ⟨l, hl⟩
Proof state after:
case intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
l : ProofList L
hl : l.isProper = true ∧ Γ ∈ l.sequents
⊢ Nonempty ( ⊢¹ Γ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
case intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
l : ProofList L
hl : l.isProper = true ∧ Γ ∈ l.sequents
⊢ Nonempty ( ⊢¹ Γ)
Tactic:
rcases derivation_of_isProper l hl.1 _ hl.2 with ⟨d⟩
Proof state after:
case intro.intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
l : ProofList L
hl : l.isProper = true ∧ Γ ∈ l.sequents
d :  ⊢¹ Γ
⊢ Nonempty ( ⊢¹ Γ)
Theorem: LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper
Proof state before:
case intro.intro
μ : Type ?u.1106645
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 μ
Γ : Sequent L
l : ProofList L
hl : l.isProper = true ∧ Γ ∈ l.sequents
d :  ⊢¹ Γ
⊢ Nonempty ( ⊢¹ Γ)
Tactic:
exact ⟨d⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
⊢ T ⊢! σ →
    ∃ l U,
      (U.all fun x => decide (T x)) = true ∧
        List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Tactic:
rintro ⟨U, hU, d⟩
Proof state after:
case intro.mk
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
case intro.mk
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Tactic:
rcases derivable_iff_isProper.mp ⟨d⟩ with ⟨l, hl, hmem⟩
Proof state after:
case intro.mk.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
case intro.mk.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Tactic:
have hl' : isProper l' := by simpa[isProper, hl] using hmem
Proof state after:
case intro.mk.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
hl' : isProper l' = true
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
case intro.mk.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
hl' : isProper l' = true
⊢ ∃ l U,
    (U.all fun x => decide (T x)) = true ∧
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true
Tactic:
exact ⟨l', U, by simpa[List.subsetSet] using hU, by simp [l'], hl'⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
⊢ isProper l' = true
Tactic:
simpa[isProper, hl] using hmem
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
hl' : isProper l' = true
⊢ (U.all fun x => decide (T x)) = true
Tactic:
simpa[List.subsetSet] using hU
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
U : List (Sentence L)
hU : ∀ p ∈ U, p ∈ T
d : U ⊢² [σ]
l : ProofList L
hl : l.isProper = true
hmem : List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ]) ∈ l.sequents
l' : List (Code L × List (Semiformula L ℕ 0)) :=
  (Code.wk (List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])),
      List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)) ::
    l
hl' : isProper l' = true
⊢ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ sequents l'
Tactic:
simp [l']
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
⊢ (∃ l U,
      (U.all fun x => decide (T x)) = true ∧
        List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents ∧ l.isProper = true) →
    T ⊢! σ
Tactic:
rintro ⟨l, U, hU, hl, hproper⟩
Proof state after:
case intro.intro.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
⊢ T ⊢! σ
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
case intro.intro.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
⊢ T ⊢! σ
Tactic:
rcases derivation_of_isProper l hproper _ hl with ⟨d⟩
Proof state after:
case intro.intro.intro.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
d :  ⊢¹ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)
⊢ T ⊢! σ
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
case intro.intro.intro.intro.intro
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
d :  ⊢¹ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)
⊢ T ⊢! σ
Tactic:
exact Gentzen.provable_iff.mpr ⟨U, by simpa using hU, ⟨Derivation.toOneSided (d.wk $ by simp)⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
d :  ⊢¹ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)
⊢ ∀ π ∈ U, π ∈ T
Tactic:
simpa using hU
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.ProofList.provable_iff
Proof state before:
μ : Type ?u.1107580
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 μ
T : Theory L
inst✝ : DecidablePred T
σ : Sentence L
l : ProofList L
U : List (Sentence L)
hU : (U.all fun x => decide (T x)) = true
hl : List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ∈ l.sequents
hproper : l.isProper = true
d :  ⊢¹ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U)
⊢ List.map (⇑Rew.emb.hom) (σ :: List.map (fun x => ~x) U) ⊆ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) U ++ [σ])
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.isSome_bool_to_opt
Proof state before:
μ : Type ?u.1166446
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 μ
b : Bool
⊢ (Bool.toOpt b).isSome = b
Tactic:
cases b <;> simp[Bool.toOpt]
Proof state after:
no goals
Theorem: LO.FirstOrder.to_opt_eq_some_iff
Proof state before:
μ : Type ?u.1167343
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 μ
b : Bool
⊢ Bool.toOpt b = some () ↔ b = true
Tactic:
cases b <;> simp[Bool.toOpt]
Proof state after:
no goals