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

State before:
μ : Type ?u.1325212
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
inst✝ : T.Computable
⊢ ∀ (n : Sentence L), provableFn T n = Part.assert ((fun x => T ⊢! x) n) fun x => Part.some ()
Tactic:
intro σ
State after:
μ : Type ?u.1325212
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
inst✝ : T.Computable
σ : Sentence L
⊢ provableFn T σ = Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()

State before:
μ : Type ?u.1325212
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
inst✝ : T.Computable
σ : Sentence L
⊢ provableFn T σ = Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Tactic:
ext
State after:
case H
μ : Type ?u.1325212
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
inst✝ : T.Computable
σ : Sentence L
a✝ : Unit
⊢ a✝ ∈ provableFn T σ ↔ a✝ ∈ Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()

State before:
case H
μ : Type ?u.1325212
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
inst✝ : T.Computable
σ : Sentence L
a✝ : Unit
⊢ a✝ ∈ provableFn T σ ↔ a✝ ∈ Part.assert ((fun x => T ⊢! x) σ) fun x => Part.some ()
Tactic:
simp[←provable_iff_provableFn]
State after:
no goals