internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
⊢ 0{L}[0] = 0 ∧ 0{L}[k / ‖I‖] = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
x✝¹ : M
x✝ : x✝¹ < k % ‖I‖
⊢ 0{L}[x✝¹ + 1] = 0{L}[x✝¹] + fbit 0 (‖I‖ * (k / ‖I‖) + x✝¹)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
⊢ 0{L}[0] = 0 ∧ 0{L}[k % ‖I‖] = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.uniq
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 k n₁ n₂ : M
H₁ : SeriesSegment U I L A k n₁
H₂ : SeriesSegment U I L A k n₂
⊢ n₁ = n₂
Tactic:
rcases H₁ with ⟨nₘ₁, _, hT₁, hS₁⟩
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n₁ n₂ : M
H₂ : SeriesSegment U I L A k n₂
nₘ₁ : M
left✝ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
⊢ n₁ = n₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.uniq
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n₁ n₂ : M
H₂ : SeriesSegment U I L A k n₂
nₘ₁ : M
left✝ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
⊢ n₁ = n₂
Tactic:
rcases H₂ with ⟨nₘ₂, _, hT₂, hS₂⟩
Proof state after:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n₁ n₂ nₘ₁ : M
left✝¹ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
nₘ₂ : M
left✝ : nₘ₂ ≤ n₂
hT₂ : Series U I L A (k / ‖I‖) nₘ₂
hS₂ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₂ n₂
⊢ n₁ = n₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.uniq
Proof state before:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n₁ n₂ nₘ₁ : M
left✝¹ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
nₘ₂ : M
left✝ : nₘ₂ ≤ n₂
hT₂ : Series U I L A (k / ‖I‖) nₘ₂
hS₂ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₂ n₂
⊢ n₁ = n₂
Tactic:
rcases show nₘ₁ = nₘ₂ from hT₁.uniq hT₂
Proof state after:
case intro.intro.intro.intro.intro.intro.refl
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 k n₁ n₂ nₘ₁ : M
left✝¹ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
left✝ : nₘ₁ ≤ n₂
hT₂ : Series U I L A (k / ‖I‖) nₘ₁
hS₂ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₂
⊢ n₁ = n₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.uniq
Proof state before:
case intro.intro.intro.intro.intro.intro.refl
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 k n₁ n₂ nₘ₁ : M
left✝¹ : nₘ₁ ≤ n₁
hT₁ : Series U I L A (k / ‖I‖) nₘ₁
hS₁ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₁
left✝ : nₘ₁ ≤ n₂
hT₂ : Series U I L A (k / ‖I‖) nₘ₁
hS₂ : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ₁ n₂
⊢ n₁ = n₂
Tactic:
exact hS₁.uniq hS₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv nₛ nₑ : M
H : Segment U L A start intv nₛ nₑ
hintv : intv < ‖I‖
hnₛ : ‖nₛ + ‖I‖‖ ≤ ‖L‖
⊢ Segment U L A start (intv + 1) nₛ (nₑ + fbit A (start + intv))
Tactic:
rcases H with ⟨S, _, H, rfl, rfl⟩
Proof state after:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
Proof state before:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Tactic:
let S' := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
Proof state after:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
Proof state before:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Tactic:
have le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖ := calc
  ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖S{L}[intv] + 1‖     := length_monotone <| by simp
  _                                    ≤ ‖S{L}[0] + intv + 1‖ := length_monotone <| by simpa using H.le_add intv (by rfl)
  _                                    ≤ ‖S{L}[0] + ‖I‖‖      := length_monotone <| by simp [add_assoc, succ_le_iff_lt, hintv]
  _                                    ≤ ‖L‖                  := hnₛ
Proof state after:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
Proof state before:
case 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
H' : IsSegment L A start (intv + 1) S'
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
Tactic:
exact
  ⟨ S',
    lt_of_lt_of_le (append_lt_sq_hash I L S (succ_le_iff_lt.mpr hintv) le_len_L (by simpa using pos_of_gt hintv)) hU,
    H',
    ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by simp),
    ext_append_last I L S (succ_le_iff_lt.mpr hintv) le_len_L ⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ S{L}[intv] + fbit A (start + intv) ≤ S{L}[intv] + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ S{L}[intv] + 1 ≤ S{L}[0] + intv + 1
Tactic:
simpa using H.le_add intv (by rfl)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ intv ≤ intv
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ S{L}[0] + intv + 1 ≤ S{L}[0] + ‖I‖
Tactic:
simp [add_assoc, succ_le_iff_lt, hintv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
⊢ IsSegment L A start (intv + 1) S'
Tactic:
intro i hi
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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi : i < intv + 1
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi : i < intv + 1
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)
Tactic:
rcases show i ≤ intv from lt_succ_iff_le.mp hi with (rfl | hi)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)

case inr
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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)
Tactic:
calc
  S'{L}[i + 1] = S{L}[i] + fbit A (start + i)  := ext_append_last I L S (succ_le_iff_lt.mpr hintv) le_len_L
  _            = S'{L}[i] + fbit A (start + i) := by congr 1; symm; exact ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S{L}[i] + fbit A (start + i) = S'{L}[i] + fbit A (start + i)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S{L}[i] = S'{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S{L}[i] = S'{L}[i]
Tactic:
symm
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S'{L}[i] = S{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ S'{L}[i] = S{L}[i]
Tactic:
exact ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start S : M
left✝ : S < U
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
i : M
hintv : i < ‖I‖
H : IsSegment L A start i S
S' : M := append I L S (i + 1) (S{L}[i] + fbit A (start + i))
le_len_L : ‖S{L}[i] + fbit A (start + i)‖ ≤ ‖L‖
hi : i < i + 1
⊢ i < i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S'{L}[i + 1] = S'{L}[i] + fbit A (start + i)
Tactic:
calc
  S'{L}[i + 1] = S{L}[i + 1]                   := ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by simpa using hi)
  _            = S{L}[i] + fbit A (start + i)  := H i hi
  _            = S'{L}[i] + fbit A (start + i) := by congr 1; symm; apply ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by assumption)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ i + 1 < intv + 1
Tactic:
simpa using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S{L}[i] + fbit A (start + i) = S'{L}[i] + fbit A (start + i)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S{L}[i] = S'{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S{L}[i] = S'{L}[i]
Tactic:
symm
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S'{L}[i] = S{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ S'{L}[i] = S{L}[i]
Tactic:
apply ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by assumption)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
i : M
hi✝ : i < intv + 1
hi : i < intv
⊢ i < intv + 1
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
H' : IsSegment L A start (intv + 1) S'
⊢ 0 < I
Tactic:
simpa using pos_of_gt hintv
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
H' : IsSegment L A start (intv + 1) S'
⊢ 0 < intv + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n n' : M
HT : Series U I L A iter n
HS : Segment U L A (‖I‖ * iter) ‖I‖ n n'
hiter : iter < ‖I‖
⊢ Series U I L A (iter + 1) n'
Tactic:
have Hn : n ≤ ‖I‖ * iter := HT.le_add
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
iter n n' : M
HT : Series U I L A iter n
HS : Segment U L A (‖I‖ * iter) ‖I‖ n n'
hiter : iter < ‖I‖
Hn : n ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'