internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.zero_lt_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 ⊧ₘ* 𝐏𝐀⁻
⊢ 0 < 1
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.zeroLtOne
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_le_of_zero_lt
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), 0 < x → 1 ≤ x
Tactic:
simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.peanoMinus.oneLeOfZeroLt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_lt_add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x < y → x + z < y + z
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addLtAdd
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), x * 0 = 0
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulZero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_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 ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), x * 1 = x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulOne
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_assoc
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x * y * z = x * (y * z)
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulAssoc
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_comm
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y : M), x * y = y * x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulComm
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_lt_mul
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x < y → 0 < z → x * z < y * z
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulLtMul
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.distr
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x * (y + z) = x * y + x * z
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.distr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_irrefl
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x : M), ¬x < x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltIrrefl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_trans
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y z : M), x < y → y < z → x < z
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltTrans
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_tri
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (x y : M), x < y ∨ x = y ∨ y < x
Tactic:
simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltTri
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_mul
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x : M
⊢ 0 * x = 0
Tactic:
simpa[mul_comm] using Model.mul_zero x
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.numeral_eq_natCast
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
⊢ ORingSymbol.numeral 1 = ↑1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.numeral_eq_natCast
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 : ℕ
⊢ ORingSymbol.numeral (n + 2) = ↑(n + 2)
Tactic:
simp[ORingSymbol.numeral, numeral_eq_natCast (n + 1), add_assoc, one_add_one_eq_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_neg
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x : M
⊢ ¬x < 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_succ_of_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x : M
h : 0 < x
⊢ ∃ y, x = y + 1
Tactic:
rcases le_iff_exists_add.mp (one_le_of_zero_lt x h) with ⟨y, 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 ⊧ₘ* 𝐏𝐀⁻
y : M
h : 0 < 1 + y
⊢ ∃ y_1, 1 + y = y_1 + 1
Theorem: LO.FirstOrder.Arith.Model.eq_succ_of_pos
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 ⊧ₘ* 𝐏𝐀⁻
y : M
h : 0 < 1 + y
⊢ ∃ y_1, 1 + y = y_1 + 1
Tactic:
exact ⟨y, add_comm 1 y⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
⊢ x ≤ y → x < y + 1
Tactic:
intro 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 ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x ≤ y
⊢ x < y + 1
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x ≤ y
⊢ x < y + 1
Tactic:
exact lt_of_le_of_lt h (lt_add_one y)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x < y + 1
⊢ x ≤ y
Tactic:
rcases lt_iff_exists_add.mp h with ⟨z, hz, h⟩
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 ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z : M
hz : z > 0
h : y + 1 = x + z
⊢ x ≤ y
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
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 ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z : M
hz : z > 0
h : y + 1 = x + z
⊢ x ≤ y
Tactic:
rcases eq_succ_of_pos hz with ⟨z', rfl⟩
Proof state after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ x ≤ y
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ x ≤ y
Tactic:
have : y = x + z' := by simpa[←add_assoc] using h
Proof state after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
this : y = x + z'
⊢ x ≤ y
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
this : y = x + z'
⊢ x ≤ y
Tactic:
simp[this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ y = x + z'
Tactic:
simpa[←add_assoc] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x : M
hx : x < ↑0
⊢ ∃ m, x = ↑m
Tactic:
simp[not_neg] at hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
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 : ℕ
x : M
hx : x < ↑(n + 1)
⊢ ∃ m, x = ↑m
Tactic:
have : x ≤ n := by simpa[le_iff_lt_succ] using 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 : ℕ
x : M
hx : x < ↑(n + 1)
this : x ≤ ↑n
⊢ ∃ m, x = ↑m
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
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 : ℕ
x : M
hx : x < ↑(n + 1)
this : x ≤ ↑n
⊢ ∃ m, x = ↑m
Tactic:
rcases this with (rfl | hx)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n : ℕ
hx : ↑n < ↑(n + 1)
⊢ ∃ m, ↑n = ↑m

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n : ℕ
x : M
hx✝ : x < ↑(n + 1)
hx : x < ↑n
⊢ ∃ m, x = ↑m
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
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 : ℕ
x : M
hx : x < ↑(n + 1)
⊢ x ≤ ↑n
Tactic:
simpa[le_iff_lt_succ] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n : ℕ
hx : ↑n < ↑(n + 1)
⊢ ∃ m, ↑n = ↑m
Tactic:
exact ⟨n, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_nat_of_lt_nat
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n : ℕ
x : M
hx✝ : x < ↑(n + 1)
hx : x < ↑n
⊢ ∃ m, x = ↑m
Tactic:
exact eq_nat_of_lt_nat hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_numeral
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 : ℕ
a✝ : Fin n
x✝ : Fin n → ℕ
⊢ Semiterm.valm M (fun x => ↑(x✝ x)) Empty.elim #a✝ = ↑(Semiterm.valm ℕ x✝ Empty.elim #a✝)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_numeral
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 : ℕ
a✝ : Fin 0 → Semiterm ℒₒᵣ Empty n
e : Fin n → ℕ
⊢ Semiterm.valm M (fun x => ↑(e x)) Empty.elim (Semiterm.func Language.Zero.zero a✝) =
    ↑(Semiterm.valm ℕ e Empty.elim (Semiterm.func Language.Zero.zero a✝))
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_numeral
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 : ℕ
a✝ : Fin 0 → Semiterm ℒₒᵣ Empty n
e : Fin n → ℕ
⊢ Semiterm.valm M (fun x => ↑(e x)) Empty.elim (Semiterm.func Language.One.one a✝) =
    ↑(Semiterm.valm ℕ e Empty.elim (Semiterm.func Language.One.one a✝))
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_numeral
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 : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n
e : Fin n → ℕ
⊢ Semiterm.valm M (fun x => ↑(e x)) Empty.elim (Semiterm.func Language.Add.add v) =
    ↑(Semiterm.valm ℕ e Empty.elim (Semiterm.func Language.Add.add v))
Tactic:
simp[Semiterm.val_func, val_numeral (v 0), val_numeral (v 1)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_numeral
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 : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n
e : Fin n → ℕ
⊢ Semiterm.valm M (fun x => ↑(e x)) Empty.elim (Semiterm.func Language.Mul.mul v) =
    ↑(Semiterm.valm ℕ e Empty.elim (Semiterm.func Language.Mul.mul v))
Tactic:
simp[Semiterm.val_func, val_numeral (v 0), val_numeral (v 1)]
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
x✝ : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ x✝) ⊤ → (Semiformula.Evalbm M fun x => ↑(x✝ x)) ⊤
Tactic:
simp
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
x✝ : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ x✝) ⊥ → (Semiformula.Evalbm M fun x => ↑(x✝ x)) ⊥
Tactic:
simp
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✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.rel op(=) v) → (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.rel op(=) v)
Tactic:
simp[Semiformula.eval_rel, Matrix.comp_vecCons', val_numeral]
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✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.nrel op(=) v) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.nrel op(=) v)
Tactic:
simp[Semiformula.eval_nrel, Matrix.comp_vecCons', val_numeral]
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✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.rel op(<) v) → (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.rel op(<) v)
Tactic:
simp[Semiformula.eval_rel, Matrix.comp_vecCons', val_numeral]
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✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.nrel op(<) v) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.nrel op(<) v)
Tactic:
simp[Semiformula.eval_nrel, Matrix.comp_vecCons', val_numeral]
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (p✝ ⋏ q✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (p✝ ⋏ q✝)
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ →
    (Semiformula.Evalbm ℕ e) q✝ → (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ →
    (Semiformula.Evalbm ℕ e) q✝ → (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
intro ep eq
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
ep : (Semiformula.Evalbm ℕ e) p✝
eq : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
ep : (Semiformula.Evalbm ℕ e) p✝
eq : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
exact ⟨pval_of_pval_nat_of_sigma_one hp ep, pval_of_pval_nat_of_sigma_one hq eq⟩
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (p✝ ⋎ q✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (p✝ ⋎ q✝)
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ ∨ (Semiformula.Evalbm ℕ e) q✝ →
    (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
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 ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ ∨ (Semiformula.Evalbm ℕ e) q✝ →
    (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
rintro (h | h)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
left
Proof state after:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝
Tactic:
exact 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:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
right
Proof state after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Theorem: LO.FirstOrder.Arith.Model.pval_of_pval_nat_of_sigma_one
Proof state before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
exact pval_of_pval_nat_of_sigma_one hq 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)
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✝