internlm/Lean-Github huggingface dataset:
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‖
Hn : n ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'
Tactic:
rcases HT with ⟨T, _, HT, Tₛ, 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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
⊢ Series U I L A (iter + 1) n'
Tactic:
let T' := append I L T (iter + 1) n'
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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ Series U I L A (iter + 1) n'
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ Series U I L A (iter + 1) n'
Tactic:
have hn'L : ‖n'‖ ≤ ‖L‖ := calc
  ‖n'‖ ≤ ‖T{L}[iter] + ‖I‖‖ := length_monotone HS.le_add
  _    ≤ ‖(iter + 1) * ‖I‖‖ := length_monotone <| by simp [add_mul, mul_comm iter, Hn]
  _    ≤ ‖‖I‖^2‖            := length_monotone <| by simp [sq]; exact mul_le_mul_right (succ_le_iff_lt.mpr hiter)
  _    ≤ ‖L‖                := hIL
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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
⊢ Series U I L A (iter + 1) n'
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
⊢ Series U I L A (iter + 1) n'
Tactic:
have hTlast : T'{L}[iter + 1] = n' := ext_append_last I L T (succ_le_iff_lt.mpr hiter) hn'L
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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
⊢ Series U I L A (iter + 1) n'
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
⊢ Series U I L A (iter + 1) n'
Tactic:
have hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l] := fun l hl ↦ ext_append_lt I L T (succ_le_iff_lt.mpr hiter) (by simp [lt_succ_iff_le, hl])
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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
⊢ Series U I L A (iter + 1) n'
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
HT' : IsSeries U I L A (iter + 1) T'
⊢ Series U I L A (iter + 1) n'
Tactic:
exact
⟨ T',
  lt_of_lt_of_le (append_lt_sq_hash I L T (succ_le_iff_lt.mpr hiter) hn'L (by simpa using pos_of_gt hiter)) hU,
  HT',
  Eq.trans (ext_append_lt I L T (succ_le_iff_lt.mpr hiter) (by simp)) Tₛ,
  hTlast ⟩
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ T{L}[iter] + ‖I‖ ≤ (iter + 1) * ‖I‖
Tactic:
simp [add_mul, mul_comm iter, Hn]
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ (iter + 1) * ‖I‖ ≤ ‖I‖ ^ 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ (iter + 1) * ‖I‖ ≤ ‖I‖ * ‖I‖
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
⊢ (iter + 1) * ‖I‖ ≤ ‖I‖ * ‖I‖
Tactic:
exact mul_le_mul_right (succ_le_iff_lt.mpr hiter)
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
l : M
hl : l ≤ iter
⊢ l < iter + 1
Tactic:
simp [lt_succ_iff_le, hl]
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
⊢ IsSeries U I L A (iter + 1) T'
Tactic:
intro l hl
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl : l < iter + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl : l < iter + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Tactic:
rcases show l ≤ iter from lt_succ_iff_le.mp hl with (rfl | hl)
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
n' T : M
left✝ : T < U
Tₛ : T{L}[0] = 0
hn'L : ‖n'‖ ≤ ‖L‖
l : M
hiter : l < ‖I‖
HT : IsSeries U I L A l T
HS : Segment U L A (‖I‖ * l) ‖I‖ (T{L}[l]) n'
Hn : T{L}[l] ≤ ‖I‖ * l
T' : M := append I L T (l + 1) n'
hTlast : T'{L}[l + 1] = n'
hTofLt : ∀ l_1 ≤ l, T'{L}[l_1] = T{L}[l_1]
hl : l < l + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])

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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
n' T : M
left✝ : T < U
Tₛ : T{L}[0] = 0
hn'L : ‖n'‖ ≤ ‖L‖
l : M
hiter : l < ‖I‖
HT : IsSeries U I L A l T
HS : Segment U L A (‖I‖ * l) ‖I‖ (T{L}[l]) n'
Hn : T{L}[l] ≤ ‖I‖ * l
T' : M := append I L T (l + 1) n'
hTlast : T'{L}[l + 1] = n'
hTofLt : ∀ l_1 ≤ l, T'{L}[l_1] = T{L}[l_1]
hl : l < l + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Tactic:
simpa [hTofLt l (by simp), hTlast] using HS
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
n' T : M
left✝ : T < U
Tₛ : T{L}[0] = 0
hn'L : ‖n'‖ ≤ ‖L‖
l : M
hiter : l < ‖I‖
HT : IsSeries U I L A l T
HS : Segment U L A (‖I‖ * l) ‖I‖ (T{L}[l]) n'
Hn : T{L}[l] ≤ ‖I‖ * l
T' : M := append I L T (l + 1) n'
hTlast : T'{L}[l + 1] = n'
hTofLt : ∀ l_1 ≤ l, T'{L}[l_1] = T{L}[l_1]
hl : l < l + 1
⊢ l ≤ l
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Tactic:
have : T'{L}[l] = T{L}[l] := hTofLt l (le_of_lt hl)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
this : T'{L}[l] = T{L}[l]
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
this : T'{L}[l] = T{L}[l]
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Tactic:
have : T'{L}[l + 1] = T{L}[l + 1] := hTofLt (l + 1) (succ_le_iff_lt.mpr hl)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
this✝ : T'{L}[l] = T{L}[l]
this : T'{L}[l + 1] = T{L}[l + 1]
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
this✝ : T'{L}[l] = T{L}[l]
this : T'{L}[l + 1] = T{L}[l + 1]
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
Tactic:
simpa [*] using HT l hl
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
HT' : IsSeries U I L A (iter + 1) T'
⊢ 0 < I
Tactic:
simpa using pos_of_gt hiter
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' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
HT' : IsSeries U I L A (iter + 1) T'
⊢ 0 < iter + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_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
a b : M
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a : M
⊢ (a + 1) / 0 = a / 0 + 1 ∧ (a + 1) % 0 = 0 ∧ a % 0 + 1 = 0 ∨ (a + 1) / 0 = a / 0 ∧ (a + 1) % 0 = a % 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_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
a b : M
pos : 0 < b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
have : a % b + 1 ≤ b := lt_iff_succ_le.mp <| mod_lt a (by simp [pos])
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
this : a % b + 1 ≤ b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_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
a b : M
pos : 0 < b
this : a % b + 1 ≤ b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
rcases this with (hb | ltb)
Proof state after:
case inr.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
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1

case inr.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
a b : M
pos : 0 < b
ltb : a % b + 1 < b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_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
a : M
⊢ (a + 1) / 0 = a / 0 + 1 ∧ (a + 1) % 0 = 0 ∧ a % 0 + 1 = 0 ∨ (a + 1) / 0 = a / 0 ∧ (a + 1) % 0 = a % 0 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_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
a b : M
pos : 0 < b
⊢ 0 < b
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.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
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
left
Proof state after:
case inr.inl.h
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
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inl.h
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
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b
Tactic:
have : b * (a / b + 1) = a + 1 := calc
  b * (a / b + 1) = b * (a / b) + a % b + 1 := by simp [hb, add_assoc, mul_add]
  _               = a + 1                   := by simp [div_add_mod a b]
Proof state after:
case inr.inl.h
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
a b : M
pos : 0 < b
hb : a % b + 1 = b
this : b * (a / b + 1) = a + 1
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b