Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re (Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
have : Partrec fun σ : Semisentence ℒₒᵣ 1 ↦ (provableFn T (~σ/[⸢σ⸣])).map (fun _ ↦ ()) :=
  Partrec.map
    ((provableFn_partrec T).comp <| Primrec.to_comp
      <| (Semiformula.neg_primrec (L := ℒₒᵣ)).comp
      <| (Semiformula.substs₁_primrec (L := ℒₒᵣ)).comp
        ((Semiterm.Operator.const_primrec (L := ℒₒᵣ)).comp
          <| (Semiterm.Operator.numeral_primrec (L := ℒₒᵣ)).comp .encode) .id)
    (.const ())
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
exact this.of_eq <| by intro σ; ext; simp[←provable_iff_provableFn]
State after:
no goals

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ ∀ (n : Semisentence ℒₒᵣ 1),
    Part.map (fun x => ()) (provableFn T (~[→ ⸢n⸣].hom n)) =
      Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) n) fun x => Part.some ()
Tactic:
intro σ
State after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
⊢ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) =
    Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
⊢ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) =
    Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Tactic:
ext
State after:
case H
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
a✝ : Unit
⊢ a✝ ∈ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) ↔
    a✝ ∈ Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()

State before:
case H
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
a✝ : Unit
⊢ a✝ ∈ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) ↔
    a✝ ∈ Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Tactic:
simp[←provable_iff_provableFn]
State after:
no goals