internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝) →
    ∀ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
      (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro h x hx
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : M
hx : x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : M
hx : x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
rcases eq_nat_of_lt_nat hx with ⟨x, rfl⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp (h x (by simpa using hx))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ x < Semiterm.val (standardModel ℕ) e Empty.elim t
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
t✝ : Semiterm ℒₒᵣ Empty (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!t✝] !p✝)”) → (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!t✝] !p✝)”)
Tactic:
rcases Rew.positive_iff.mp pt with ⟨t, rfl⟩
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”)
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”)
Tactic:
simp[val_numeral]
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t,
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
        (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t,
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
        (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro x hx h
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
    (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
    (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
exact ⟨x, by simpa using hx, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (∃' p) → (Semiformula.Evalbm M fun x => ↑(e x)) (∃' p)
Tactic:
simp
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
intro x h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
have : Hierarchy 𝚺 1 p := hp.accum _
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
exact ⟨x, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one this h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one this h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (∃' p✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (∃' p✝)
Tactic:
simp
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro x hx
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
exact ⟨x, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.sigma_one_completeness
Proof state before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
haveI : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_provably_subtheory M 𝐏𝐀⁻ T inferInstance (by assumption)
Proof state after:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.Arith.sigma_one_completeness
Proof state before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ σ
Tactic:
simpa [Matrix.empty_eq] using Model.pval_of_pval_nat_of_sigma_one (M := M) hσ H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.sigma_one_completeness
Proof state before:
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ* T
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.subset_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ ⊆ t₂ ↔ t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ ↔ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
. intro h; cases h; simp;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
. rintro ⟨h₁, h₂⟩; cases t₁; cases t₂; simp_all;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h : t₁ = t₂
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h : t₁ = t₂
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
cases h
Proof state after:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ : Tableau α
⊢ t₁.1 = t₁.1 ∧ t₁.2 = t₁.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ : Tableau α
⊢ t₁.1 = t₁.1 ∧ t₁.2 = t₁.2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
rintro ⟨h₁, h₂⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h₁ : t₁.1 = t₂.1
h₂ : t₁.2 = t₂.2
⊢ t₁ = t₂
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h₁ : t₁.1 = t₂.1
h₂ : t₁.2 = t₂.2
⊢ t₁ = t₂
Tactic:
cases t₁
Proof state after:
case mpr.intro.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₂ : Tableau α
fst✝ snd✝ : Theory α
h₁ : (fst✝, snd✝).1 = t₂.1
h₂ : (fst✝, snd✝).2 = t₂.2
⊢ (fst✝, snd✝) = t₂
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mpr.intro.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₂ : Tableau α
fst✝ snd✝ : Theory α
h₁ : (fst✝, snd✝).1 = t₂.1
h₂ : (fst✝, snd✝).2 = t₂.2
⊢ (fst✝, snd✝) = t₂
Tactic:
cases t₂
Proof state after:
case mpr.intro.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
fst✝¹ snd✝¹ fst✝ snd✝ : Theory α
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def
Proof state before:
case mpr.intro.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
fst✝¹ snd✝¹ fst✝ snd✝ : Theory α
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₁
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (𝓓)-Consistent (insert p T, U) ↔
    ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj'
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (𝓓)-Consistent (insert p T, U) →
    ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj') →
    (𝓓)-Consistent (insert p T, U)
Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₁
Proof state before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (𝓓)-Consistent (insert p T, U) →
    ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj') →
    (𝓓)-Consistent (insert p T, U)
Tactic:
. intro h Γ Δ hΓ hΔ;
  by_contra hC;
  have : 𝓓 ⊬! (p :: Γ).conj' ⟶ Δ.disj' := h (by simp; intro q hq; right; exact hΓ q hq;) hΔ;
  have : 𝓓 ⊢! (p :: Γ).conj' ⟶ Δ.disj' := implyLeft_cons_conj'!.mpr hC;
  contradiction;
Proof state after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
p : Formula α
T U : Theory α
⊢ (∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → 𝓓 ⊬! p ⋏ Γ.conj' ⟶ Δ.disj') →
    (𝓓)-Consistent (insert p T, U)