internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
⊢ Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
Tactic:
simpa [hdiv] using HT.succ hU hIL this (lt_iff_succ_le.mpr $ by simpa [hdiv] using hhk)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
⊢ k / ‖I‖ + 1 ≤ ‖I‖
Tactic:
simpa [hdiv] using hhk
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ n + fbit A k ≤ n + fbit A k
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) (n + fbit A k) (n + fbit A k)
Tactic:
simp [hmodsucc]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) 0 (n + fbit A k) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) 0 (n + fbit A k) (n + fbit A k)
Tactic:
apply Segment.refl U L A
Proof state after:
case hL
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ L # 1 ≤ U

case hn
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ ‖n + fbit A k‖ ≤ ‖L‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case hL
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ L # 1 ≤ U
Tactic:
calc
  L # 1 ≤ I # L     := by rw [hash_comm L 1]; apply hash_monotone (pos_iff_one_le.mp Ipos) (by rfl)
  _     ≤ (I # L)^2 := by simp
  _     ≤ U         := hU
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ L # 1 ≤ I # L
Tactic:
rw [hash_comm L 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ 1 # L ≤ I # L
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ 1 # L ≤ I # L
Tactic:
apply hash_monotone (pos_iff_one_le.mp Ipos) (by rfl)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ L ≤ L
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ I # L ≤ (I # L) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case hn
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ ‖n + fbit A k‖ ≤ ‖L‖
Tactic:
calc
  ‖n + fbit A k‖ ≤ ‖n + 1‖ := length_monotone <| by simp
  _              ≤ ‖k + 1‖ := length_monotone <| by simp [hnk]
  _              ≤ ‖‖I‖^2‖ := length_monotone <| succ_le_iff_lt.mpr hk
  _              ≤ ‖L‖     := hIL
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ n + fbit A k ≤ n + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ n + 1 ≤ k + 1
Tactic:
simp [hnk]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k) := by
  simpa [div_add_mod, hdiv, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
Proof state after:
case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have HT' : Series U I L A ((k + 1) / ‖I‖) nₘ := by simpa [hdiv] using HT
Proof state after:
case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
HT' : Series U I L A ((k + 1) / ‖I‖) nₘ
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
HT' : Series U I L A ((k + 1) / ‖I‖) nₘ
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
exact ⟨nₘ, le_trans hnₘn le_self_add, HT', HS'⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
⊢ Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
Tactic:
simpa [div_add_mod, hdiv, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
⊢ 0 < ‖I‖
Tactic:
simp [Ipos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
HS' : Segment U L A (‖I‖ * ((k + 1) / ‖I‖)) ((k + 1) % ‖I‖) nₘ (n + fbit A k)
⊢ Series U I L A ((k + 1) / ‖I‖) nₘ
Tactic:
simpa [hdiv] using HT
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.len_polyI
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 [length_two_mul_of_pos pos, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_le
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‖ < ‖polyI A‖ ^ 2
Tactic:
simp [len_polyI pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.two_add_two_eq_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
⊢ 2 + 2 = 4
Tactic:
simp [←three_add_one_eq_four, ←two_add_one_eq_three, ←one_add_one_eq_two, add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_eq_two_mul_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 : M
⊢ 4 * a = 2 * (2 * a)
Tactic:
simp [←two_add_two_eq_four, add_mul, two_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.two_mul_sqrt_le_self
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) ^ 2 + 1 ≤ a + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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
⊢ (4 * a) # (4 * a) ≤ ((4 * a) # (2 * a)) ^ 2
Tactic:
simp [four_mul_eq_two_mul_two_mul, hash_two_mul_le_sq_hash]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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
⊢ ((4 * a) # (2 * a)) ^ 2 ≤ ((4 * a) # a) ^ 4
Tactic:
simp [pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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
⊢ ((4 * a) # a) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4
Tactic:
rw [hash_comm (4 * a) 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
⊢ (a # (4 * a)) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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 # (4 * a)) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4
Tactic:
simp [four_mul_eq_two_mul_two_mul, pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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 # (2 * a)) ^ 2) ^ 4 ≤ ((a # a) ^ 4) ^ 4
Tactic:
simp [pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self
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) ^ 4) ^ 4 ≤ (a # a) ^ 16
Tactic:
simp [←pow_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
h : 0 < √a
⊢ √a ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
⊢ 0 < a → 0 < √a
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
h : 0 < a
⊢ 0 < √a
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
h : 0 < a
⊢ 0 < √a
Tactic:
by_contra 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
h : 0 < a
A : ¬0 < √a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
h : 0 < a
A : ¬0 < √a
⊢ False
Tactic:
simp at 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
h : 0 < a
A : √a = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
h : 0 < a
A : √a = 0
⊢ False
Tactic:
simp [show a = 0 from by simpa [A] using sqrt_lt_sq a] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.pos_sq_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 : M
h : 0 < a
A : √a = 0
⊢ a = 0
Tactic:
simpa [A] using sqrt_lt_sq a
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.pow_four_le_pow_four
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 ^ 4 ≤ b ^ 4 ↔ a ≤ b
Tactic:
simp [pow_four_eq_sq_sq]
Proof state after:
no goals