internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
μ : Type ?u.1169140
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 ⊢! σ ↔ ∃ e, isProofFn T σ e = true
Tactic:
simp[provable_iff, isProofFn]
Proof state after:
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) ↔
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) ↔
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true
Tactic:
constructor
Proof state after:
case mp
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) →
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true

case mpr
μ : Type ?u.1169140
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
⊢ (∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true) →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mp
μ : Type ?u.1169140
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, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true) →
    ∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true
Tactic:
rintro ⟨l, U, hU, hl, hproper⟩
Proof state after:
case mp.intro.intro.intro.intro
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ ∃ e,
    Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
      true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mp.intro.intro.intro.intro
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ ∃ e,
    Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
      true
Tactic:
use encode (l, U)
Proof state after:
case h
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ Option.rec false
      (fun val =>
        (val.2.all fun x => decide (T x)) &&
            decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
          val.1.isProper)
      ((decode (encode (l, U)).unpair.1).bind fun a => Option.map (Prod.mk a) (decode (encode (l, U)).unpair.2)) =
    true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case h
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
this : (U.all fun x => decide (T x)) = true
⊢ Option.rec false
      (fun val =>
        (val.2.all fun x => decide (T x)) &&
            decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
          val.1.isProper)
      ((decode (encode (l, U)).unpair.1).bind fun a => Option.map (Prod.mk a) (decode (encode (l, U)).unpair.2)) =
    true
Tactic:
simp[hU, hl, hproper, this]
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ (U.all fun x => decide (T x)) = true
Tactic:
simp
Proof state after:
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ ∀ x ∈ U, T x
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
⊢ ∀ x ∈ U, T x
Tactic:
intro x hx
Proof state after:
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
x : Sentence L
hx : x ∈ U
⊢ T x
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
μ : Type ?u.1169140
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 : ∀ x ∈ U, T x
hl : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
hproper : l.isProper = true
x : Sentence L
hx : x ∈ U
⊢ T x
Tactic:
exact hU x hx
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr
μ : Type ?u.1169140
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
⊢ (∃ e,
      Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
        true) →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
simp
Proof state after:
case mpr
μ : Type ?u.1169140
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
⊢ ∀ (x : ℕ),
    Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode x.unpair.1).bind fun a => Option.map (Prod.mk a) (decode x.unpair.2)) =
        true →
      ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr
μ : Type ?u.1169140
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
⊢ ∀ (x : ℕ),
    Option.rec false
          (fun val =>
            (val.2.all fun x => decide (T x)) &&
                decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
              val.1.isProper)
          ((decode x.unpair.1).bind fun a => Option.map (Prod.mk a) (decode x.unpair.2)) =
        true →
      ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
intro e
Proof state after:
case mpr
μ : Type ?u.1169140
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
e : ℕ
⊢ Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
      true →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr
μ : Type ?u.1169140
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
e : ℕ
⊢ Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        ((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)) =
      true →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
rcases decode e.unpair.1 with (_ | ⟨l⟩) <;> simp
Proof state after:
case mpr.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
⊢ Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        (Option.map (Prod.mk l) (decode e.unpair.2)) =
      true →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
⊢ Option.rec false
        (fun val =>
          (val.2.all fun x => decide (T x)) &&
              decide (Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) val.2 ∈ val.1.sequents) &&
            val.1.isProper)
        (Option.map (Prod.mk l) (decode e.unpair.2)) =
      true →
    ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
rcases decode e.unpair.2 with (_ | ⟨U⟩) <;> simp
Proof state after:
case mpr.some.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
U : List (Sentence L)
⊢ (∀ x ∈ U, T x) →
    Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents →
      l.isProper = true →
        ∃ l U,
          (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr.some.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
U : List (Sentence L)
⊢ (∀ x ∈ U, T x) →
    Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents →
      l.isProper = true →
        ∃ l U,
          (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
intro h₁ h₂ h₃
Proof state after:
case mpr.some.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
U : List (Sentence L)
h₁ : ∀ x ∈ U, T x
h₂ : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
h₃ : l.isProper = true
⊢ ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Theorem: LO.FirstOrder.provable_iff_isProofFn
Proof state before:
case mpr.some.some
μ : Type ?u.1169140
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
e : ℕ
l : ProofList L
U : List (Sentence L)
h₁ : ∀ x ∈ U, T x
h₂ : Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents
h₃ : l.isProper = true
⊢ ∃ l U, (∀ x ∈ U, T x) ∧ Rew.emb.hom σ :: List.map (⇑Rew.emb.hom ∘ fun x => ~x) U ∈ l.sequents ∧ l.isProper = true
Tactic:
exact ⟨l, U, h₁, h₂, h₃⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
μ : Type ?u.1286883
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 : Unit
⊢ T ⊢! σ ↔ u ∈ provableFn T σ
Tactic:
rcases u with ⟨⟩
Proof state after:
case unit
μ : Type ?u.1286883
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 ⊢! σ ↔ PUnit.unit ∈ provableFn T σ
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit
μ : Type ?u.1286883
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 ⊢! σ ↔ PUnit.unit ∈ provableFn T σ
Tactic:
simp[provableFn, provable_iff_isProofFn, Nat.rfindOpt, @eq_comm _ true, @eq_comm _ false]
Proof state after:
case unit
μ : Type ?u.1286883
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
⊢ (∃ e, isProofFn T σ e = true) ↔
    ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Theorem: LO.FirstOrder.provable_iff_provableFn
Proof state before:
case unit
μ : Type ?u.1286883
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
⊢ (∃ e, isProofFn T σ e = true) ↔
    ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
constructor
Proof state after:
case unit.mp
μ : Type ?u.1286883
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
⊢ (∃ e, isProofFn T σ e = true) →
    ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true

case unit.mpr
μ : Type ?u.1286883
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
⊢ (∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true) →
    ∃ e, isProofFn T σ e = true