internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
⊢ Seqₛ (2 * y ^ 2) X' Y'
Tactic:
intro j hj jne2 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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
by_cases hjy : j ≤ y
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : j ≤ y
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : j ≤ y
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
have : Seqₛ y X' Y' := hseqₛ.append ppi (by simp [←hYy, ppi.pos])
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : j ≤ y
this : Seqₛ y X' Y'
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : j ≤ y
this : Seqₛ y X' Y'
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
exact this j hjy jne2 ppj
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : j ≤ y
⊢ y < i
Tactic:
simp [←hYy, ppi.pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
have : i = j := by
  have : Pow2 y := by simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
  exact PPow2.two_mul_sq_uniq this ppi ppj
    ⟨by simp [←hYy, ppi.pos], le_trans hi (by simp)⟩ ⟨by simpa using hjy, hj⟩
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : i = j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : i = j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
rcases this with rfl
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i ∨ Seqₛ.Odd X' Y' i
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i ∨ Seqₛ.Odd X' Y' i
Tactic:
right
Proof state after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Odd X' Y' i
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Odd X' Y' i
Tactic:
simp [Seqₛ.Odd]
Proof state after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ ext (i ^ 2) X' = 2 * ext i X' + 1 ∧ ext (i ^ 2) Y' = 2 * ext i Y' ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ 2 * y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ ext (i ^ 2) X' = 2 * ext i X' + 1 ∧ ext (i ^ 2) Y' = 2 * ext i Y' ^ 2
Tactic:
rw [ext_append_last, ext_append_last, ext_append_of_lt , ext_append_of_lt] <;>
  simp [ppi, ppi.sq, hxsqi, hysqi, hiisq, hXx, hYy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
⊢ i = j
Tactic:
have : Pow2 y := by simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ i = j
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ i = j
Tactic:
exact PPow2.two_mul_sq_uniq this ppi ppj
  ⟨by simp [←hYy, ppi.pos], le_trans hi (by simp)⟩ ⟨by simpa using hjy, hj⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
⊢ Pow2 y
Tactic:
simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ y < i
Tactic:
simp [←hYy, ppi.pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ y ^ 2 ≤ 2 * y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ 2 * y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ y < j
Tactic:
simpa using hjy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (2 * y ^ 2) X' Y'
⊢ y ^ 2 ≤ 2 * y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (2 * y ^ 2) X' Y'
⊢ ext (i ^ 2) X' = 2 * x + 1 ∧ ext (i ^ 2) Y' = 2 * y ^ 2
Tactic:
simp [X', Y']
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (2 * y ^ 2) X' Y'
⊢ ext (i ^ 2) (append (i ^ 2) X (2 * x + 1)) = 2 * x + 1 ∧ ext (i ^ 2) (append (i ^ 2) Y (2 * y ^ 2)) = 2 * y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
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 X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (2 * y ^ 2) X' Y'
⊢ ext (i ^ 2) (append (i ^ 2) X (2 * x + 1)) = 2 * x + 1 ∧ ext (i ^ 2) (append (i ^ 2) Y (2 * y ^ 2)) = 2 * y ^ 2
Tactic:
rw [ext_append_last, ext_append_last] <;> try simp [hxsqi, hysqi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case hz
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x + 1 < i ^ 2
hysqi : 2 * y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x + 1)
Y' : M := append (i ^ 2) Y (2 * y ^ 2)
bX' : X' ≤ (2 * y ^ 2) ^ 4
bY' : Y' ≤ (2 * y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (2 * y ^ 2) X' Y'
⊢ 2 * x + 1 < i ^ 2
Tactic:
simp [hxsqi, hysqi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd
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 : M
⊢ (∃ y', y = 2 * y' ^ 2 ∧ Exponential x y') → Exponential (2 * x + 1) y
Tactic:
rintro ⟨y, rfl, h⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
exact bit_one h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd_two_mul_sq
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 : M
⊢ Exponential (2 * x + 1) (2 * y ^ 2) → Exponential x y
Tactic:
intro h
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 : M
h : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd_two_mul_sq
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 : M
h : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ Exponential x y
Tactic:
rcases exponential_exists_sq_of_exponential_odd h with ⟨y', e, h⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h✝ : Exponential (2 * x + 1) (2 * y ^ 2)
y' : M
e : 2 * y ^ 2 = 2 * y' ^ 2
h : Exponential x y'
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd_two_mul_sq
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h✝ : Exponential (2 * x + 1) (2 * y ^ 2)
y' : M
e : 2 * y ^ 2 = 2 * y' ^ 2
h : Exponential x y'
⊢ Exponential x y
Tactic:
simpa [show y = y' from by simpa using e] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_odd_two_mul_sq
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 : M
h✝ : Exponential (2 * x + 1) (2 * y ^ 2)
y' : M
e : 2 * y ^ 2 = 2 * y' ^ 2
h : Exponential x y'
⊢ y = y'
Tactic:
simpa using e
Proof state after:
no goals