internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof 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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
have : bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 ∣ p :=
  Pow2.dvd_of_le (by simp; apply bexp_pow2 lt_len) pp (this.monotone_le (exponential_of_pow2 pp) (le_log_of_lt_length h))
Proof 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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this✝ : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
this : bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 ∣ p
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof 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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this✝ : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
this : bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 ∣ p
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
rcases this with ⟨q, hq⟩
Proof state after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
calc
  (S₁ + S₂ * p){L}[i] = (S₁ + p * S₂) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1         := by simp [ext, mul_comm S₂]
  _                   = (S₁ + bexp (S₁ + S₂ * p) (i * ‖L‖) * (L # 1 * q * S₂)) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1 := by simp [←mul_assoc, ←hq]
  _                   = (S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) + L # 1 * q * S₂) % L # 1 := by rw [div_add_mul_self' _ _ (bexp_pos lt_len)]
  _                   = S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1                    := by simp [mul_assoc]
  _                   = S₁{L}[i]                                                     := ext_eq_of_ge le_self_add
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof 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 i S₁ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
⊢ (S₁ + 0 * p){L}[i] = S₁{L}[i]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
⊢ i ≤ i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
Tactic:
simp [add_mul]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ Exponential (i * ‖L‖ + ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ Exponential (i * ‖L‖ + ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
Tactic:
exact Exponential.add_mul (by simp [lt_len]) (by simpa using exponential_hash L 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ Exponential (i * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖))
Tactic:
simp [lt_len]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ Exponential ‖L‖ (L # 1)
Tactic:
simpa using exponential_hash L 1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
⊢ Pow2 (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
Tactic:
simp
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
⊢ Pow2 (bexp (S₁ + S₂ * p) (i * ‖L‖))
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
⊢ Pow2 (bexp (S₁ + S₂ * p) (i * ‖L‖))
Tactic:
apply bexp_pow2 lt_len
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + S₂ * p){L}[i] = (S₁ + p * S₂) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1
Tactic:
simp [ext, mul_comm S₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + p * S₂) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1 =
    (S₁ + bexp (S₁ + S₂ * p) (i * ‖L‖) * (L # 1 * q * S₂)) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1
Tactic:
simp [←mul_assoc, ←hq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ + bexp (S₁ + S₂ * p) (i * ‖L‖) * (L # 1 * q * S₂)) / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1 =
    (S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) + L # 1 * q * S₂) % L # 1
Tactic:
rw [div_add_mul_self' _ _ (bexp_pos lt_len)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
this : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1)
q : M
hq : p = bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1 * q
⊢ (S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) + L # 1 * q * S₂) % L # 1 = S₁ / bexp (S₁ + S₂ * p) (i * ‖L‖) % L # 1
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_bexp
Proof 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 i j S₁ S₂ : M
hi : i ≤ ‖I‖
hij : j < i
⊢ (j + 1) * ‖L‖ < ‖bexp (I # L) (i * ‖L‖)‖
Tactic:
rw [len_bexp (mul_len_lt_len_hash hi), lt_succ_iff_le]
Proof 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 i j S₁ S₂ : M
hi : i ≤ ‖I‖
hij : j < i
⊢ (j + 1) * ‖L‖ ≤ i * ‖L‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_bexp
Proof 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 i j S₁ S₂ : M
hi : i ≤ ‖I‖
hij : j < i
⊢ (j + 1) * ‖L‖ ≤ i * ‖L‖
Tactic:
exact mul_le_mul_right (succ_le_iff_lt.mpr hij)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)){L}[i + j] = S₂{L}[j]
Tactic:
have hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖)) := exp_bexp_of_lt (mul_len_lt_len_hash $ le_trans le_self_add hij)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)){L}[i + j] = S₂{L}[j]
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)){L}[i + j] = S₂{L}[j]
Tactic:
calc  (S₁ + S₂ * bexp (I # L) (i * ‖L‖)){L}[i + j]
    = (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) ((i + j) * ‖L‖) % (L # 1)                    := by rw [ext_eq_hash_of_le hij]
  _ = (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖) / bexp (I # L) (j * ‖L‖) % (L # 1) := by
    simp [←div_mul, add_mul]; congr 2; exact bexp_add (by simp [←add_mul, mul_len_lt_len_hash hij])
  _ = S₂ / bexp (I # L) (j * ‖L‖) % (L # 1)                                                          := by
    congr 2; rw [div_add_mul_self, div_eq_zero_of_lt] <;> simp [hie.lt_iff_len_le.mpr hS₁, hie.range_pos]
  _ = S₂{L}[j]                                                                                       := ext_eq_hash_of_le (le_trans le_add_self hij)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)){L}[i + j] =
    (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) ((i + j) * ‖L‖) % L # 1
Tactic:
rw [ext_eq_hash_of_le hij]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) ((i + j) * ‖L‖) % L # 1 =
    (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖) / bexp (I # L) (j * ‖L‖) % L # 1
Tactic:
simp [←div_mul, add_mul]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖ + j * ‖L‖) % L # 1 =
    (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / (bexp (I # L) (i * ‖L‖) * bexp (I # L) (j * ‖L‖)) % L # 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖ + j * ‖L‖) % L # 1 =
    (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / (bexp (I # L) (i * ‖L‖) * bexp (I # L) (j * ‖L‖)) % L # 1
Tactic:
congr 2
Proof state after:
case e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ bexp (I # L) (i * ‖L‖ + j * ‖L‖) = bexp (I # L) (i * ‖L‖) * bexp (I # L) (j * ‖L‖)
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
case e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ bexp (I # L) (i * ‖L‖ + j * ‖L‖) = bexp (I # L) (i * ‖L‖) * bexp (I # L) (j * ‖L‖)
Tactic:
exact bexp_add (by simp [←add_mul, mul_len_lt_len_hash hij])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ i * ‖L‖ + j * ‖L‖ < ‖I # L‖
Tactic:
simp [←add_mul, mul_len_lt_len_hash hij]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖) / bexp (I # L) (j * ‖L‖) % L # 1 =
    S₂ / bexp (I # L) (j * ‖L‖) % L # 1
Tactic:
congr 2
Proof state after:
case e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖) = S₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₂_bexp
Proof state before:
case e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L I i j S₁ S₂ : M
hij : i + j ≤ ‖I‖
hS₁ : ‖S₁‖ ≤ i * ‖L‖
hie : Exponential (i * ‖L‖) (bexp (I # L) (i * ‖L‖))
⊢ (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) / bexp (I # L) (i * ‖L‖) = S₂
Tactic:
rw [div_add_mul_self, div_eq_zero_of_lt] <;> simp [hie.lt_iff_len_le.mpr hS₁, hie.range_pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_nil
Proof 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
⊢ append I L S i 0 = S % bexp (I # L) (i * ‖L‖)
Tactic:
simp [append]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.len_append
Proof 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 : 0 < X
⊢ ‖append I L S i X‖ = ‖X * bexp (I # L) (i * ‖L‖) + S % bexp (I # L) (i * ‖L‖)‖
Tactic:
simp [append, add_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.len_append
Proof 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 : 0 < X
⊢ ‖X‖ + log (bexp (I # L) (i * ‖L‖)) = ‖X‖ + i * ‖L‖
Tactic:
simp [log_bexp (mul_len_lt_len_hash hi)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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]
Proof 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‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_hash
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.append_lt_sq_hash
Proof 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
Proof state after:
no goals