Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_eq_of_ge (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 S S' i : M
h : S ≤ S'
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
rcases show i * ‖L‖ < ‖S‖ ∨ ‖S‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S‖ with (lt | le)
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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 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 S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
unfold ext
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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1

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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S / bexp S (i * ‖L‖) % L # 1
Tactic:
congr 2
State after:
case inl.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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)

State before:
case inl.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 S S' i : M
h : S ≤ S'
lt : i * ‖L‖ < ‖S‖
⊢ bexp S' (i * ‖L‖) = bexp S (i * ‖L‖)
Tactic:
exact bexp_eq_of_lt_length (lt_of_lt_of_le lt $ length_monotone h) lt
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 S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = S{L}[i]
Tactic:
simp [ext_eq_zero_of_lt le]
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 S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

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 S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
rcases show i * ‖L‖ < ‖S'‖ ∨ ‖S'‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S'‖ with (lt' | le')
State after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
le' : ‖S'‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

State before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
have : S < bexp S' (i * ‖L‖) := ((exp_bexp_of_lt lt').lt_iff_len_le).mpr le
State after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

State before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
this : S < bexp S' (i * ‖L‖)
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
simp [this]
State after:
no goals

State before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
le' : ‖S'‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
Tactic:
simp [bexp_eq_zero_of_le le']
State after:
no goals