Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
⊢ Seqₛ y' (X % i) (Y % i)
Tactic:
intro j hj ne2 ppj
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j
Tactic:
have : j^2 < i := lt_of_le_of_lt (sq_le_sq.mpr hj) hi
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this : j ^ 2 < i
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this : j ^ 2 < i
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j
Tactic:
have : j < i := lt_of_le_of_lt (le_trans hj $ by simp) hi
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j
Tactic:
rcases h j (le_trans hj hy) ne2 ppj with (H | H)
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 ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Even X Y j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Odd X Y j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this : j ^ 2 < i
⊢ y' ≤ y' ^ 2
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Even X Y j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j
Tactic:
left
State after:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Even X Y j
⊢ Even (X % i) (Y % i) j

State before:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Even X Y j
⊢ Even (X % i) (Y % i) j
Tactic:
simpa [Seqₛ.Even, ext_rem, ppj, ppj.sq, ppi, *] using H
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 ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Odd X Y j
⊢ Even (X % i) (Y % i) j ∨ Odd (X % i) (Y % i) j
Tactic:
right
State after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Odd X Y j
⊢ Odd (X % i) (Y % i) j

State before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y y' X Y i : M
h : Seqₛ y X Y
ppi : PPow2 i
hi : y' ^ 2 < i
hy : y' ≤ y
j : M
hj : j ≤ y'
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j ^ 2 < i
this : j < i
H : Odd X Y j
⊢ Odd (X % i) (Y % i) j
Tactic:
simpa [Seqₛ.Odd, ext_rem, ppj, ppj.sq, ppi, *] using H
State after:
no goals