Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_add₁_pow2 (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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
rcases zero_le S₂ 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
⊢ (S₁ + 0 * p){L}[i] = S₁{L}[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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]

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₂
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
have lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖ := calc
      i * ‖L‖ ≤ (i + 1) * ‖L‖ := mul_le_mul_right (by simp)
      _       < ‖p‖           := h
      _       ≤ ‖S₁ + S₂ * p‖ := length_monotone (le_add_left (le_mul_of_pos_left 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]

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‖
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]
Tactic:
have : Exponential ((i + 1) * ‖L‖) (bexp (S₁ + S₂ * p) (i * ‖L‖) * L # 1) := by
  simp [add_mul]
  exact Exponential.add_mul (by simp [lt_len]) (by simpa using exponential_hash L 1)
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)
⊢ (S₁ + S₂ * p){L}[i] = S₁{L}[i]

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

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

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

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
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 i S₁ S₂ p : M
pp : Pow2 p
h : (i + 1) * ‖L‖ < ‖p‖
pos₂ : 0 < S₂
⊢ i ≤ i + 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 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]
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)

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

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