Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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
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⟩
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))

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

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

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

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

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

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

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

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

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