internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_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 a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ bexp a (4 * x) = bexp a' x ^ 4
Tactic:
rw [four_mul_eq_two_mul_two_mul, bexp_two_mul (a' := a), bexp_two_mul (a := a), pow_four_eq_sq_sq]
Proof state after:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖

case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ x < ‖a'‖

case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * (2 * x) < ‖a‖

case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_mul
Proof state before:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖
Tactic:
exact lt_of_le_of_lt (by simp [four_mul_eq_two_mul_two_mul]) hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_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 a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x ≤ 4 * x
Tactic:
simp [four_mul_eq_two_mul_two_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_mul
Proof state before:
case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ x < ‖a'‖
Tactic:
exact hx'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_mul
Proof state before:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * (2 * x) < ‖a‖
Tactic:
simpa [four_mul_eq_two_mul_two_mul] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_mul
Proof state before:
case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖
Tactic:
exact lt_of_le_of_lt (by simp [four_mul_eq_two_mul_two_mul]) hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ bexp (polyI A # polyI A) ((√‖A‖ + 1) ^ 2) = polyI A # polyI A
Tactic:
simpa [sq, len_polyI pos] using bexp_eq_hash (polyI A) (polyI A)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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 < ‖polyI A # polyI A‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ (2 * √‖A‖) ^ 2 < ‖(2 * A) # (2 * A)‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos, length_two_mul_of_pos pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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 ≤ (2 * √‖A‖) ^ 2
Tactic:
simp [two_mul, ←pos_iff_one_le, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ bexp ((2 * A) # (2 * A)) ((2 * √‖A‖) ^ 2) ≤ bexp ((2 * A) # (2 * A)) (4 * (√‖A‖) ^ 2)
Tactic:
simp [mul_pow, two_pow_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ 4 * (√‖A‖) ^ 2 < ‖(2 * A) # (2 * A)‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos, length_two_mul_of_pos pos, ←two_pow_two_eq_four, ←mul_pow]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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 < ‖A # 1‖
Tactic:
simp [length_hash, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ^ 4 ≤ bexp (A # 1) ‖A‖ ^ 4
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 : M
pos : 0 < A
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ≤ bexp (A # 1) ‖A‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ≤ bexp (A # 1) ‖A‖
Tactic:
exact (bexp_monotone_le (by simp [length_hash, lt_succ_iff_le]) (by simp [length_hash, lt_succ_iff_le])).mpr (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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 # 1‖
Tactic:
simp [length_hash, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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 ≤ ‖A‖
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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
⊢ bexp (A # 1) ‖A‖ ^ 4 = (A # 1) ^ 4
Tactic:
congr 1
Proof state after:
case e_a
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
⊢ bexp (A # 1) ‖A‖ = A # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
Proof state before:
case e_a
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
⊢ bexp (A # 1) ‖A‖ = A # 1
Tactic:
simpa using bexp_eq_hash A 1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded
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) ^ 4 ≤ (2 * A + 1) ^ 4
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ polyI A ≤ polyI A
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ polyL A ≤ 3 * polyI A
Tactic:
simp [polyL, sq_len_le_three_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ 0 < 4
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ 3 ≤ 4
Tactic:
simp [←three_add_one_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ (4 * polyI A) # (4 * polyI A) ≤ (polyI A # polyI A) ^ (4 * 4)
Tactic:
simpa using four_mul_hash_self _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ (polyI A # polyI A) ^ (4 * 4) ≤ ((2 * A + 1) ^ 4) ^ (4 * 4)
Tactic:
simp only [pow_mul, pow_four_le_pow_four, polyI_hash_self_polybounded pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded
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
⊢ ((2 * A + 1) ^ 4) ^ (4 * 4) = (2 * A + 1) ^ 64
Tactic:
simp [←pow_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.sq_polyI_hash_polyL_polybounded
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
⊢ (polyI A # polyL A) ^ 2 ≤ ((2 * A + 1) ^ 64) ^ 2
Tactic:
simp [polyI_hash_polyL_polybounded pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.sq_polyI_hash_polyL_polybounded
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
⊢ ((2 * A + 1) ^ 64) ^ 2 = polyU A
Tactic:
simp [polyU, ←pow_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ Defined (fun v => IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) isSegmentDef
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 5 → M
⊢ (fun v => IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isSegmentDef)
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 5 → M
⊢ (fun v => IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isSegmentDef)
Tactic:
simp [IsSegment, isSegmentDef, ext_defined.df.iff, fbit_defined.df.iff, lt_succ_iff_le, numeral_eq_natCast]
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 5 → M
⊢ (∀ i < v 3, v 4{v 0}[i + 1] = v 4{v 0}[i] + fbit (v 1) (v 2 + i)) ↔
    ∀ x < v 3,
      ∃ x_1 ≤ v 4,
        x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 5 → M
⊢ (∀ i < v 3, v 4{v 0}[i + 1] = v 4{v 0}[i] + fbit (v 1) (v 2 + i)) ↔
    ∀ x < v 3,
      ∃ x_1 ≤ v 4,
        x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Tactic:
apply forall₂_congr
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
⊢ ∀ a < v 3,
    v 4{v 0}[a + 1] = v 4{v 0}[a] + fbit (v 1) (v 2 + a) ↔
      ∃ x ≤ v 4,
        x = v 4{v 0}[a + 1] ∧ ∃ x_1 ≤ v 4, x_1 = v 4{v 0}[a] ∧ ∃ x_2 < 2, x_2 = fbit (v 1) (v 2 + a) ∧ x = x_1 + x_2
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
⊢ ∀ a < v 3,
    v 4{v 0}[a + 1] = v 4{v 0}[a] + fbit (v 1) (v 2 + a) ↔
      ∃ x ≤ v 4,
        x = v 4{v 0}[a + 1] ∧ ∃ x_1 ≤ v 4, x_1 = v 4{v 0}[a] ∧ ∃ x_2 < 2, x_2 = fbit (v 1) (v 2 + a) ∧ x = x_1 + x_2
Tactic:
intro x _
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x) ↔
    ∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x) ↔
    ∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Tactic:
constructor
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x) →
    ∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ (∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧
        ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3) →
    v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x) →
    ∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Tactic:
intro h
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ ∃ x_1 ≤ v 4,
    x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ ∃ x_1 ≤ v 4,
    x_1 = v 4{v 0}[x + 1] ∧ ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3
Tactic:
exact ⟨_, by simp, rfl, _, by simp, rfl, _, by simp, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 5 → M
x : M
b✝ : x < v 3
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ v 4{v 0}[x + 1] ≤ v 4
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 5 → M
x : M
b✝ : x < v 3
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ v 4{v 0}[x] ≤ v 4
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_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 5 → M
x : M
b✝ : x < v 3
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ fbit (v 1) (v 2 + x) < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 5 → M
x : M
b✝ : x < v 3
⊢ (∃ x_1 ≤ v 4,
      x_1 = v 4{v 0}[x + 1] ∧
        ∃ x_2 ≤ v 4, x_2 = v 4{v 0}[x] ∧ ∃ x_3 < 2, x_3 = fbit (v 1) (v 2 + x) ∧ x_1 = x_2 + x_3) →
    v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
Tactic:
rintro ⟨_, _, rfl, _, _, rfl, _, _, rfl, h⟩
Proof state after:
case h.mpr.intro.intro.intro.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 5 → M
x : M
b✝ : x < v 3
left✝² : v 4{v 0}[x + 1] ≤ v 4
left✝¹ : v 4{v 0}[x] ≤ v 4
left✝ : fbit (v 1) (v 2 + x) < 2
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSegmentDef_defined
Proof state before:
case h.mpr.intro.intro.intro.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 5 → M
x : M
b✝ : x < v 3
left✝² : v 4{v 0}[x + 1] ≤ v 4
left✝¹ : v 4{v 0}[x] ≤ v 4
left✝ : fbit (v 1) (v 2 + x) < 2
h : v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
⊢ v 4{v 0}[x + 1] = v 4{v 0}[x] + fbit (v 1) (v 2 + x)
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.segmentDef_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ Defined (fun v => Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) segmentDef
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 7 → M
⊢ (fun v => Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val segmentDef)
Theorem: LO.FirstOrder.Arith.Model.Nuon.segmentDef_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 7 → M
⊢ (fun v => Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val segmentDef)
Tactic:
simp [Segment, segmentDef, ext_defined.df.iff, isSegmentDef_defined.df.iff, @Eq.comm _ (v 5), @Eq.comm _ (v 6)]
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 7 → M
⊢ (∃ S < v 0, IsSegment (v 1) (v 2) (v 3) (v 4) S ∧ S{v 1}[0] = v 5 ∧ S{v 1}[v 4] = v 6) ↔
    ∃ x < v 0, IsSegment (v 1) (v 2) (v (Fin.succ 2)) (v 4) x ∧ x{v 1}[0] = v 5 ∧ x{v 1}[v 4] = v 6
Theorem: LO.FirstOrder.Arith.Model.Nuon.segmentDef_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 7 → M
⊢ (∃ S < v 0, IsSegment (v 1) (v 2) (v 3) (v 4) S ∧ S{v 1}[0] = v 5 ∧ S{v 1}[v 4] = v 6) ↔
    ∃ x < v 0, IsSegment (v 1) (v 2) (v (Fin.succ 2)) (v 4) x ∧ x{v 1}[0] = v 5 ∧ x{v 1}[v 4] = v 6
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ (∃ a ≤ z, a = b ∧ p a) → b ≤ z ∧ p b
Tactic:
rintro ⟨a, hp, rfl, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a ≤ z
hr : p a
⊢ a ≤ z ∧ p a
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_le_iff
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a ≤ z
hr : p a
⊢ a ≤ z ∧ p a
Tactic:
exact ⟨hp, hr⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ b ≤ z ∧ p b → ∃ a ≤ z, a = b ∧ p a
Tactic:
rintro ⟨hp, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b ≤ z
hr : p b
⊢ ∃ a ≤ z, a = b ∧ p a
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_le_iff
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b ≤ z
hr : p b
⊢ ∃ a ≤ z, a = b ∧ p a
Tactic:
exact ⟨b, hp, rfl, hr⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_lt_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ (∃ a < z, a = b ∧ p a) → b < z ∧ p b
Tactic:
rintro ⟨a, hp, rfl, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a < z
hr : p a
⊢ a < z ∧ p a
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_lt_iff
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
a : M
hp : a < z
hr : p a
⊢ a < z ∧ p a
Tactic:
exact ⟨hp, hr⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_lt_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
⊢ b < z ∧ p b → ∃ a < z, a = b ∧ p a
Tactic:
rintro ⟨hp, hr⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b < z
hr : p b
⊢ ∃ a < z, a = b ∧ p a
Theorem: LO.FirstOrder.Arith.Model.Nuon.bex_eq_lt_iff
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z : M
p : M → Prop
b : M
hp : b < z
hr : p b
⊢ ∃ a < z, a = b ∧ p a
Tactic:
exact ⟨b, hp, rfl, hr⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.isSerieDef_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ Defined (fun v => IsSeries (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) isSeriesDef
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 6 → M
⊢ (fun v => IsSeries (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isSeriesDef)