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

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

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

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

State before:
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
Tactic:
intro h
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
h : ∃ e, isProofFn T σ e = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true

State before:
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
h : ∃ e, isProofFn T σ e = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
rcases Nat.least_number _ h with ⟨e, he, hm⟩
State after:
case unit.mp.intro.intro
μ : 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
h : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true

State before:
case unit.mp.intro.intro
μ : 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
h : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
⊢ ∃ a, (isProofFn T σ a = true ∧ ∀ {m : ℕ}, m < a → isProofFn T σ m = false) ∧ isProofFn T σ a = true
Tactic:
exact ⟨e, ⟨he, fun h => by simpa using hm _ h⟩, he⟩
State after:
no goals

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
h✝ : ∃ e, isProofFn T σ e = true
e : ℕ
he : isProofFn T σ e = true
hm : ∀ z < e, ¬isProofFn T σ z = true
m✝ : ℕ
h : m✝ < e
⊢ isProofFn T σ m✝ = false
Tactic:
simpa using hm _ h
State after:
no goals

State before:
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
Tactic:
rintro ⟨e, ⟨he, _⟩, _⟩
State after:
case unit.mpr.intro.intro.intro
μ : 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 : ℕ
right✝¹ he : isProofFn T σ e = true
right✝ : ∀ {m : ℕ}, m < e → isProofFn T σ m = false
⊢ ∃ e, isProofFn T σ e = true

State before:
case unit.mpr.intro.intro.intro
μ : 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 : ℕ
right✝¹ he : isProofFn T σ e = true
right✝ : ∀ {m : ℕ}, m < e → isProofFn T σ m = false
⊢ ∃ e, isProofFn T σ e = true
Tactic:
exact ⟨e, he⟩
State after:
no goals