internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Relation Exponential via exponentialDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 2 → M
⊢ (fun v => Exponential (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val exponentialDef)
Theorem: LO.FirstOrder.Arith.Model.Exponential.defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 2 → M
⊢ (fun v => Exponential (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val exponentialDef)
Tactic:
simp [Exponential.graph_iff, exponentialDef, ppow2_defined.df.iff, ext_defined.df.iff,
Exponential.Seqₛ.defined.df.iff, ←le_iff_lt_succ, pow_four, sq, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_lt_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 1 < 4
Tactic:
rw [←three_add_one_eq_four]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 1 < 3 + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_lt_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 1 < 3 + 1
Tactic:
exact lt_add_of_pos_left 1 three_pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_lt_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 < 3
Tactic:
rw [←two_add_one_eq_three]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 < 2 + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_lt_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 < 2 + 1
Tactic:
exact lt_add_one 2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.three_lt_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 3 < 4
Tactic:
rw [←three_add_one_eq_four]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 3 < 3 + 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.three_lt_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 3 < 3 + 1
Tactic:
exact lt_add_one 3
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.seq₀_zero_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Seq₀ seqX₀ seqY₀
Tactic:
simp [seqX₀, seqY₀, Seq₀, ext, one_lt_four, two_lt_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.rem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i : M
h : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ Seq₀ (X % i) (Y % i)
Tactic:
rw [Seq₀, ext_rem, ext_rem] <;> try simp [ppi, hi]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i : M
h : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ ext 4 X = 1 ∧ ext 4 Y = 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.rem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i : M
h : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ ext 4 X = 1 ∧ ext 4 Y = 2
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.rem
Proof state before:
case hij
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i : M
h : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ 4 < i
Tactic:
simp [ppi, hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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)
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 ⊧ₘ* 𝐈𝚫₀
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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
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 ⊧ₘ* 𝐈𝚫₀
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
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 ⊧ₘ* 𝐈𝚫₀
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.rem
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.seqₛ_one_zero_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Seqₛ 1 seqX₀ seqY₀
Tactic:
intro u leu
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u : M
leu : u ≤ 1
⊢ u ≠ 2 → PPow2 u → Seqₛ.Even seqX₀ seqY₀ u ∨ Seqₛ.Odd seqX₀ seqY₀ u
Theorem: LO.FirstOrder.Arith.Model.Exponential.seqₛ_one_zero_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u : M
leu : u ≤ 1
⊢ u ≠ 2 → PPow2 u → Seqₛ.Even seqX₀ seqY₀ u ∨ Seqₛ.Odd seqX₀ seqY₀ u
Tactic:
rcases le_one_iff_eq_zero_or_one.mp leu with (rfl | rfl) <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.append_lt
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 X z : M
hz : z < i
⊢ X % i + z * i < (1 + z) * i
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 ⊧ₘ* 𝐈𝚫₀
i X z : M
hz : z < i
⊢ X % i < i
Theorem: LO.FirstOrder.Arith.Model.Exponential.append_lt
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 X z : M
hz : z < i
⊢ X % i < i
Tactic:
exact mod_lt _ (pos_of_gt hz)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.append_lt
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 X z : M
hz : z < i
⊢ (1 + z) * i ≤ i ^ 2
Tactic:
simp [sq, add_comm]
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 X z : M
hz : z < i
⊢ (z + 1) * i ≤ i * i
Theorem: LO.FirstOrder.Arith.Model.Exponential.append_lt
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 X z : M
hz : z < i
⊢ (z + 1) * i ≤ i * i
Tactic:
exact mul_le_mul_of_nonneg_right (lt_iff_succ_le.mp hz) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.append_lt
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 X z : M
hz : z < i
⊢ 0 ≤ i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_last
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 X z : M
hz : z < i
⊢ ext i (append i X z) = z
Tactic:
simp [ext, append, div_add_mul_self, show 0 < i from pos_of_gt hz, hz]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_of_lt
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
⊢ ext i (append j X z) = ext i X
Tactic:
have : i^2 ∣ j := Pow2.dvd_of_le hi.pow2.sq hj.pow2 (PPow2.sq_le_of_lt hi hj 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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (append j X z) = ext i X
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_of_lt
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (append j X z) = ext i X
Tactic:
calc
  ext i (append j X z) = ext i ((X % j) + z * j)       := rfl
  _                    = ext i (X % j)                 := ext_add_of_dvd_sq_right hi.pos (Dvd.dvd.mul_left this z)
  _                    = ext i (j * (X / j) + (X % j)) := by rw [add_comm]; refine Eq.symm <| ext_add_of_dvd_sq_right hi.pos (Dvd.dvd.mul_right this _)
  _                    = ext i X                         := by simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_of_lt
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (X % j) = ext i (j * (X / j) + X % j)
Tactic:
rw [add_comm]
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (X % j) = ext i (X % j + j * (X / j))
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_of_lt
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (X % j) = ext i (X % j + j * (X / j))
Tactic:
refine Eq.symm <| ext_add_of_dvd_sq_right hi.pos (Dvd.dvd.mul_right this _)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_append_of_lt
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 j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
X z : M
this : i ^ 2 ∣ j
⊢ ext i (j * (X / j) + X % j) = ext i X
Tactic:
simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.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 ⊧ₘ* 𝐈𝚫₀
X Y i x y : M
H : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ Seq₀ (Exponential.append i X x) (Exponential.append i Y y)
Tactic:
rw [Seq₀, ext_append_of_lt, ext_append_of_lt] <;> try simp [ppi, hi]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i x y : M
H : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ ext 4 X = 1 ∧ ext 4 Y = 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.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 ⊧ₘ* 𝐈𝚫₀
X Y i x y : M
H : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ ext 4 X = 1 ∧ ext 4 Y = 2
Tactic:
exact H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seq₀.append
Proof state before:
case hij
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
X Y i x y : M
H : Seq₀ X Y
ppi : PPow2 i
hi : 4 < i
⊢ 4 < i
Tactic:
simp [ppi, hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
⊢ Seqₛ z (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y)
Tactic:
intro j hj ne2 ppj
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Tactic:
have : j < i^2 := lt_of_lt_of_le (lt_of_le_of_lt hj hz) (by 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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this : j < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this : j < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Tactic:
have : j^2 < i^2 := sq_lt_sq.mpr (lt_of_le_of_lt hj hz)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
Tactic:
rcases h j hj ne2 ppj with (H | H) <;> simp [Even, Odd]
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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2 ∨
    ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2 ∨
    ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
⊢ i ≤ i ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2 ∨
    ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2
Tactic:
left
Proof 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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
    ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof 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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
    ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2
Tactic:
rw [ext_append_of_lt, ext_append_of_lt, ext_append_of_lt, ext_append_of_lt] <;> try simp [ppi.sq, ppj.sq, lt_of_le_of_lt hj hz, *]
Proof 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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) X = 2 * ext j X ∧ ext (j ^ 2) Y = ext j Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof 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 ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) X = 2 * ext j X ∧ ext (j ^ 2) Y = ext j Y ^ 2
Tactic:
exact H
Proof state after:
no goals