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

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
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
hi : i < ‖I‖
⊢ append I L S i X < (I # L) ^ 2

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 X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ append I L S ‖I‖ X < (I # L) ^ 2
Tactic:
calc
  append I L S ‖I‖ X = S % I # L + X * I # L := by simp [append, bexp_eq_hash]
  _                  < (X + 1) * I # L       := by simp [add_mul, add_comm]
  _                  ≤ L # 1 * I # L         := mul_le_mul_right (succ_le_iff_lt.mpr $ lt_hash_one_iff.mpr hX)
  _                  ≤ (I # L) ^ 2           := by simp [sq, hash_comm L 1]; exact 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ append I L S ‖I‖ X = S % I # L + X * I # L
Tactic:
simp [append, bexp_eq_hash]
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 X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ S % I # L + X * I # L < (X + 1) * I # L
Tactic:
simp [add_mul, add_comm]
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 X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ L # 1 * I # L ≤ (I # L) ^ 2
Tactic:
simp [sq, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ 1 # L ≤ I # L
Tactic:
exact 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
⊢ L ≤ L
Tactic:
rfl
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
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
hi : i < ‖I‖
⊢ append I L S i X < (I # L) ^ 2
Tactic:
exact lt_of_lt_of_le (append_lt_hash I L S hi hX) (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 X : M
hX : ‖X‖ ≤ ‖L‖
Ipos : 0 < I
hi : i < ‖I‖
⊢ I # L ≤ (I # L) ^ 2
Tactic:
simp
State after:
no goals