Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hhk : (k + 1)/‖I‖ ≤ ‖I‖ := by simpa using div_monotone (succ_le_iff_lt.mpr hk) ‖I‖
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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hnk : n ≤ k := H.le
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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have Ipos : 0 < I := by simpa using pos_of_gt hk
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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
rcases H with ⟨nₘ, hnₘn, HT, HS⟩
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 : 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
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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 : 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
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖ := by
  have : k / ‖I‖ < ‖I‖ := div_lt_of_lt_mul (by simpa [sq] using hk)
  calc
    ‖nₘ + ‖I‖‖ ≤ ‖‖I‖ * (k / ‖I‖ + 1)‖ := length_monotone <| by simp [mul_add, HT.le_add]
    _        ≤ ‖‖I‖^2‖                 := length_monotone <| by simp[sq]; exact mul_le_mul_left (lt_iff_succ_le.mp this)
    _        ≤ ‖L‖                     := hIL
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 : 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‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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 : 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‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
rcases div_mod_succ k ‖I‖ with (⟨hdiv, hmodsucc, hmod⟩ | ⟨hdiv, hmod⟩)
State after:
case intro.intro.intro.inl.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
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‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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)

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
H : SeriesSegment U I L A k n
⊢ (k + 1) / ‖I‖ ≤ ‖I‖
Tactic:
simpa using div_monotone (succ_le_iff_lt.mpr hk) ‖I‖
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
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ 0 < I
Tactic:
simpa using pos_of_gt hk
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
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
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖
Tactic:
have : k / ‖I‖ < ‖I‖ := div_lt_of_lt_mul (by simpa [sq] using hk)
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
this : k / ‖I‖ < ‖I‖
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖

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
this : k / ‖I‖ < ‖I‖
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖
Tactic:
calc
  ‖nₘ + ‖I‖‖ ≤ ‖‖I‖ * (k / ‖I‖ + 1)‖ := length_monotone <| by simp [mul_add, HT.le_add]
  _        ≤ ‖‖I‖^2‖                 := length_monotone <| by simp[sq]; exact mul_le_mul_left (lt_iff_succ_le.mp this)
  _        ≤ ‖L‖                     := hIL
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
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
⊢ k < ‖I‖ * ‖I‖
Tactic:
simpa [sq] using hk
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
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
this : k / ‖I‖ < ‖I‖
⊢ nₘ + ‖I‖ ≤ ‖I‖ * (k / ‖I‖ + 1)
Tactic:
simp [mul_add, HT.le_add]
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
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
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖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
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
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖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
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
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖I‖ * ‖I‖
Tactic:
exact mul_le_mul_left (lt_iff_succ_le.mp this)
State after:
no goals

State before:
case intro.intro.intro.inl.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
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‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k) := by
  simpa [div_add_mod, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
State after:
case intro.intro.intro.inl.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
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)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

State before:
case intro.intro.intro.inl.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
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)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k) := by
  simpa [hdiv] using HT.succ hU hIL this (lt_iff_succ_le.mpr $ by simpa [hdiv] using hhk)
State after:
case intro.intro.intro.inl.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
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)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

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‖
⊢ Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
Tactic:
simpa [div_add_mod, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
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
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‖
⊢ 0 < ‖I‖
Tactic:
simp [Ipos]
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
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)
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
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
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
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
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
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]
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)

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

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

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

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

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

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

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