internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
have : ‖x‖ * ‖y‖ < ‖z‖ :=
  lt_of_le_of_lt (by simp [sq]; exact mul_le_mul_right (length_monotone le)) h.lt_length
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this : ‖x‖ * ‖y‖ < ‖z‖
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this : ‖x‖ * ‖y‖ < ‖z‖
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
have : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖)) := exp_bexp_of_lt (a := z) (x := ‖x‖ * ‖y‖) this
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this✝ : ‖x‖ * ‖y‖ < ‖z‖
this : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖))
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
this✝ : ‖x‖ * ‖y‖ < ‖z‖
this : Exponential (‖x‖ * ‖y‖) (bexp z (‖x‖ * ‖y‖))
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
exact ExistsUnique.intro (bexp z (‖x‖ * ‖y‖)) this (fun z' H' ↦ H'.uniq this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁] (x y : M), x ≤ y → ∃! z, Exponential (‖x‖ * ‖y‖) z
le : ¬x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
simpa [mul_comm] using this y x (le_of_not_ge le)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖x‖ * ‖y‖ ≤ ‖y‖ ^ 2
Tactic:
simp [sq]
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖x‖ * ‖y‖ ≤ ‖y‖ * ‖y‖
Theorem: LO.FirstOrder.Arith.Model.hash_exists_unique
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ‖x‖ * ‖y‖ ≤ ‖y‖ * ‖y‖
Tactic:
exact mul_le_mul_right (length_monotone le)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exponential_hash_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 : M
⊢ Exponential ‖a‖ (a # 1)
Tactic:
simpa using exponential_hash a 1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ 𝚺₀-Function₂ Hash.hash via hashDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => v 0 # v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val hashDef)
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => v 0 # v 1) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val hashDef)
Tactic:
simp[hashDef, length_defined.df.iff, Exponential.defined.df.iff, ←le_iff_lt_succ]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 # v 2 ↔ ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 # v 2 ↔ ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 # v 2 → ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ (∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)) → v 0 = v 1 # v 2
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ v 0 = v 1 # v 2 → ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)
Tactic:
intro h
Proof state after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ ∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)
Tactic:
exact ⟨‖v 1‖, by simp, ‖v 2‖, by simp, rfl, rfl, by rw [h]; exact exponential_hash _ _⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ ‖v 1‖ ≤ v 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ ‖v 2‖ ≤ v 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ Exponential (‖v 1‖ * ‖v 2‖) (v 0)
Tactic:
rw [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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ Exponential (‖v 1‖ * ‖v 2‖) (v 1 # v 2)
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
h : v 0 = v 1 # v 2
⊢ Exponential (‖v 1‖ * ‖v 2‖) (v 1 # v 2)
Tactic:
exact exponential_hash _ _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
⊢ (∃ x ≤ v 1, ∃ x_1 ≤ v 2, x = ‖v 1‖ ∧ x_1 = ‖v 2‖ ∧ Exponential (x * x_1) (v 0)) → v 0 = v 1 # v 2
Tactic:
rintro ⟨_, _, _, _, rfl, rfl, h⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
left✝¹ : ‖v 1‖ ≤ v 1
left✝ : ‖v 2‖ ≤ v 2
h : Exponential (‖v 1‖ * ‖v 2‖) (v 0)
⊢ v 0 = v 1 # v 2
Theorem: LO.FirstOrder.Arith.Model.hash_defined
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin (Nat.succ 2) → M
left✝¹ : ‖v 1‖ ≤ v 1
left✝ : ‖v 2‖ ≤ v 2
h : Exponential (‖v 1‖ * ‖v 2‖) (v 0)
⊢ v 0 = v 1 # v 2
Tactic:
exact h.uniq (exponential_hash (v 1) (v 2))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_zero_left
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 : M
⊢ Exponential (‖0‖ * ‖a‖) 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_zero_right
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 : M
⊢ Exponential (‖a‖ * ‖0‖) 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
⊢ Exponential (‖a‖ * ‖b‖) (b # a)
Tactic:
simpa [mul_comm] using exponential_hash b a
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_right
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 : M
⊢ a < a # 1
Tactic:
have : Exponential ‖a‖ (a # 1) := by simpa using (exponential_hash a 1)
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 : M
this : Exponential ‖a‖ (a # 1)
⊢ a < a # 1
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_right
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 : M
this : Exponential ‖a‖ (a # 1)
⊢ a < a # 1
Tactic:
exact lt_exponential_length this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_right
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 : M
⊢ Exponential ‖a‖ (a # 1)
Tactic:
simpa using (exponential_hash a 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
⊢ a # 1 ≤ 2 * a + 1
Tactic:
rcases zero_le a with (rfl | pos)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ 0 # 1 ≤ 2 * 0 + 1

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
pos : 0 < a
⊢ a # 1 ≤ 2 * a + 1
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ 0 # 1 ≤ 2 * 0 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
⊢ a # 1 ≤ 2 * a + 1
Tactic:
exact (le_iff_lt_length_of_exp (exponential_hash a 1)).mpr (by
  simp [mul_comm 2 a]
  have : ‖a * 2 + 1‖ = ‖a‖ + 1 := by
    simpa using length_mul_pow2_add_of_lt pos (show Pow2 2 from by simp) one_lt_two
  simp [this])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
⊢ ‖a‖ * ‖1‖ < ‖2 * a + 1‖
Tactic:
simp [mul_comm 2 a]
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 : M
pos : 0 < a
⊢ ‖a‖ < ‖a * 2 + 1‖
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
⊢ ‖a‖ < ‖a * 2 + 1‖
Tactic:
have : ‖a * 2 + 1‖ = ‖a‖ + 1 := by
  simpa using length_mul_pow2_add_of_lt pos (show Pow2 2 from by simp) one_lt_two
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 : M
pos : 0 < a
this : ‖a * 2 + 1‖ = ‖a‖ + 1
⊢ ‖a‖ < ‖a * 2 + 1‖
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
this : ‖a * 2 + 1‖ = ‖a‖ + 1
⊢ ‖a‖ < ‖a * 2 + 1‖
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
⊢ ‖a * 2 + 1‖ = ‖a‖ + 1
Tactic:
simpa using length_mul_pow2_add_of_lt pos (show Pow2 2 from by simp) one_lt_two
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_righs
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 : M
pos : 0 < a
⊢ Pow2 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_le_iff
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 b c : M
⊢ ¬b # c ≤ a ↔ ¬‖b‖ * ‖c‖ < ‖a‖
Tactic:
simp [lt_hash_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_hash_one_iff
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 b : M
⊢ a < b # 1 ↔ ‖a‖ ≤ ‖b‖
Tactic:
simpa using lt_hash_iff (a := a) (b := b) (c := 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_monotone
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₁ a₂ b₁ b₂ : M
h₁ : a₁ ≤ b₁
h₂ : a₂ ≤ b₂
⊢ 0 ≤ ‖a₂‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_monotone
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₁ a₂ b₁ b₂ : M
h₁ : a₁ ≤ b₁
h₂ : a₂ ≤ b₂
⊢ 0 ≤ ‖b₁‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bexp_eq_hash
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 b : M
⊢ ‖a‖ * ‖b‖ < ‖a # b‖
Tactic:
simp [length_hash]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_two_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
⊢ a # (2 * b) = a # b * a # 1
Tactic:
have h₁ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b)) := by
  simpa [length_two_mul_of_pos pos, mul_add] using exponential_hash a (2 * b)
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 b : M
pos : 0 < b
h₁ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b))
⊢ a # (2 * b) = a # b * a # 1
Theorem: LO.FirstOrder.Arith.Model.hash_two_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
h₁ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b))
⊢ a # (2 * b) = a # b * a # 1
Tactic:
have h₂ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # b * a # 1) := (exponential_hash a b).add_mul (exponential_hash_one a)
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 b : M
pos : 0 < b
h₁ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b))
h₂ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # b * a # 1)
⊢ a # (2 * b) = a # b * a # 1
Theorem: LO.FirstOrder.Arith.Model.hash_two_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
h₁ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b))
h₂ : Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # b * a # 1)
⊢ a # (2 * b) = a # b * a # 1
Tactic:
exact h₁.uniq h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_two_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
⊢ Exponential (‖a‖ * ‖b‖ + ‖a‖) (a # (2 * b))
Tactic:
simpa [length_two_mul_of_pos pos, mul_add] using exponential_hash a (2 * b)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_two_mul_le_sq_hash
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 b : M
⊢ a # (2 * b) ≤ (a # b) ^ 2
Tactic:
rcases zero_le b with (rfl | pos)
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 : M
⊢ a # (2 * 0) ≤ (a # 0) ^ 2

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
⊢ a # (2 * b) ≤ (a # b) ^ 2
Theorem: LO.FirstOrder.Arith.Model.hash_two_mul_le_sq_hash
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 : M
⊢ a # (2 * 0) ≤ (a # 0) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_two_mul_le_sq_hash
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 b : M
pos : 0 < b
⊢ a # (2 * b) ≤ (a # b) ^ 2
Tactic:
simp [hash_two_mul a pos, sq]
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a b : M
pos : 0 < b
⊢ a # 1 ≤ a # b
Theorem: LO.FirstOrder.Arith.Model.hash_two_mul_le_sq_hash
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 b : M
pos : 0 < b
⊢ a # 1 ≤ a # b
Tactic:
exact hash_monotone (by rfl) (pos_iff_one_le.mp pos)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_two_mul_le_sq_hash
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 b : M
pos : 0 < b
⊢ a ≤ a
Tactic:
rfl
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_sigma
Proof state before:
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : HSemiformula L ξ n (𝚫, m)
⊢ p.sigma.val = p.val
Tactic:
rcases p
Proof state after:
case mkDelta
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, m)
a✝ : HSemiformula L ξ n (𝚷, m)
⊢ (a✝¹.mkDelta a✝).sigma.val = (a✝¹.mkDelta a✝).val
Theorem: Arith.HSemiformula.val_sigma
Proof state before:
case mkDelta
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, m)
a✝ : HSemiformula L ξ n (𝚷, m)
⊢ (a✝¹.mkDelta a✝).sigma.val = (a✝¹.mkDelta a✝).val
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_mkPolarity
Proof state before:
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : Semiformula L ξ n
Γ : Polarity
h : Hierarchy Γ m p
⊢ (mkPolarity p Γ h).val = p
Tactic:
cases Γ <;> rfl
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.iff'
Proof state before:
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : HSemisentence L n (𝚫, m)
h : ProperOn M p
e : Fin n → M
⊢ (Semiformula.Evalbm M e) (pi p).val ↔ (Semiformula.Evalbm M e) (val p)
Tactic:
simp [←h.iff, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.iff'
Proof state before:
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : HSemiformula L M n (𝚫, m)
h : ProperWithParamOn M p
e : Fin n → M
⊢ (Semiformula.Evalm M e id) p.pi.val ↔ (Semiformula.Evalm M e id) p.val
Tactic:
simp [←h.iff, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_rew
Proof state before:
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
Γ : HierarchySymbol
p : HSemiformula L ξ₁ n₁ Γ
⊢ (rew ω p).val = ω.hom p.val
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ₁ n₁ (Γ, m)
⊢ (rew ω p).val = ω.hom p.val
Theorem: Arith.HSemiformula.val_rew
Proof state before:
case mk
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ₁ n₁ (Γ, m)
⊢ (rew ω p).val = ω.hom p.val
Tactic:
rcases p with (_ | _ | ⟨⟨p, _⟩, ⟨q, _⟩⟩) <;> simp [rew]
Proof state after:
no goals