Theorem: LO.FirstOrder.provable_iff_isProofFn (Logic/FirstOrder/Computability/Calculus.lean)

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]
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

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
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

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⟩
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

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)
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

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]
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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₃
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

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₃⟩
State after:
no goals