Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
⊢ append I L S i X < I # L
Tactic:
rcases zero_le X with (rfl | pos)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i : M
hi : i < ‖I‖
hX : ‖0‖ ≤ ‖L‖
⊢ append I L S i 0 < I # L

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
pos : 0 < X
⊢ append I L S i X < I # L

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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i : M
hi : i < ‖I‖
hX : ‖0‖ ≤ ‖L‖
⊢ append I L S i 0 < I # L
Tactic:
simp [append_nil]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i : M
hi : i < ‖I‖
hX : ‖0‖ ≤ ‖L‖
⊢ S % bexp (I # L) (i * ‖L‖) < I # L

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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i : M
hi : i < ‖I‖
hX : ‖0‖ ≤ ‖L‖
⊢ S % bexp (I # L) (i * ‖L‖) < I # L
Tactic:
exact lt_of_lt_of_le (mod_lt _ (bexp_pos $ mul_len_lt_len_hash $ le_of_lt hi)) (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i : M
hi : i < ‖I‖
hX : ‖0‖ ≤ ‖L‖
⊢ bexp (I # L) (i * ‖L‖) ≤ I # 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
pos : 0 < X
⊢ append I L S i X < I # L
Tactic:
simp [lt_hash_iff, len_append I L S (le_of_lt hi) pos]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
pos : 0 < X
⊢ ‖X‖ + i * ‖L‖ ≤ ‖I‖ * ‖L‖

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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
pos : 0 < X
⊢ ‖X‖ + i * ‖L‖ ≤ ‖I‖ * ‖L‖
Tactic:
calc
  ‖X‖ + i * ‖L‖ ≤ (i + 1) * ‖L‖ := by simp [add_mul, add_comm (i * ‖L‖), hX]
  _             ≤ ‖I‖ * ‖L‖     := mul_le_mul_right (succ_le_iff_lt.mpr 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i < ‖I‖
hX : ‖X‖ ≤ ‖L‖
pos : 0 < X
⊢ ‖X‖ + i * ‖L‖ ≤ (i + 1) * ‖L‖
Tactic:
simp [add_mul, add_comm (i * ‖L‖), hX]
State after:
no goals