Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.succ (Arithmetization/OmegaOne/Nuon.lean)

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
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'

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⟩
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'

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'
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'

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
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'

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
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'

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])
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'

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 ⟩
State after:
no goals

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]
State after:
no goals

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]
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‖

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)
State after:
no goals

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]
State after:
no goals

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
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])

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)
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])

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
State after:
no goals

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
State after:
no goals

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)
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])

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)
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])

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals