internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have hysqi : 2 * y ^ 2 < i ^ 2 := by
  have : 2 * ext i Y ≤ i := two_mul_ext_le_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
  suffices 2 * (2 * y ^ 2) < 2 * i ^ 2 from lt_of_mul_lt_mul_left this
  calc
    2 * (2 * y ^ 2) = (2 * y)^2 := by simp [sq, mul_assoc, mul_left_comm y 2]
    _               ≤ i^2       := sq_le_sq.mpr (by simpa [hYy] using this)
    _               < 2 * i^2   := lt_mul_of_one_lt_left ppi.sq.pos one_lt_two
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have hiisq : i < i^2 := lt_square_of_lt ppi.one_lt
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
let X' := append (i^2) X (2 * x + 1)
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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)
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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)
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
let Y' := append (i^2) Y (2 * (y^2))
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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)
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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)
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have bX' : X' ≤ (2 * y ^ 2)^4 := by
  have : X' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
  exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) (le_trans hi $ by simp) 4)
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have bY' : Y' ≤ (2 * y ^ 2)^4 := by
  have : Y' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
  exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) (le_trans hi $ by simp) 4)
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have hseq₀' : Seq₀ X' Y' := hseq₀.append ppi.sq (ppi.sq.four_lt ppi.sq_ne_two (ppi.sq_ne_four ne2))
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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'
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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'
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
have hseqₘ' : Seqₘ (2 * x + 1) (2 * y ^ 2) X' Y' :=
  ⟨i ^ 2, sq_le_sq.mpr (le_trans hi $ by simp), ppi.sq_ne_two, ppi.sq,
   by simp [X', Y']; rw [ext_append_last, ext_append_last] <;> try simp [hxsqi, hysqi]⟩
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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'
hseqₘ' : Seqₘ (2 * x + 1) (2 * y ^ 2) X' Y'
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 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'
hseqₘ' : Seqₘ (2 * x + 1) (2 * y ^ 2) X' Y'
⊢ Exponential (2 * x + 1) (2 * y ^ 2)
Tactic:
exact Or.inr <| ⟨X', bX', Y', bY', hseq₀', hseqₛ', hseqₘ'⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
hx : x = 0
⊢ Exponential (2 * x + 1) (2 * 1 ^ 2)
Tactic:
rcases hx with rfl
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential (2 * 0 + 1) (2 * 1 ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_one
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential (2 * 0 + 1) (2 * 1 ^ 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
⊢ 2 * x + 1 < 2 * i + 1
Tactic:
simp [←hXx, 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
⊢ 2 * y ^ 2 < i ^ 2
Tactic:
have : 2 * ext i Y ≤ i := two_mul_ext_le_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
this : 2 * ext i Y ≤ i
⊢ 2 * y ^ 2 < i ^ 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
this : 2 * ext i Y ≤ i
⊢ 2 * y ^ 2 < i ^ 2
Tactic:
suffices 2 * (2 * y ^ 2) < 2 * i ^ 2 from lt_of_mul_lt_mul_left this
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
this : 2 * ext i Y ≤ i
⊢ 2 * (2 * y ^ 2) < 2 * i ^ 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
this : 2 * ext i Y ≤ i
⊢ 2 * (2 * y ^ 2) < 2 * i ^ 2
Tactic:
calc
  2 * (2 * y ^ 2) = (2 * y)^2 := by simp [sq, mul_assoc, mul_left_comm y 2]
  _               ≤ i^2       := sq_le_sq.mpr (by simpa [hYy] using this)
  _               < 2 * i^2   := lt_mul_of_one_lt_left ppi.sq.pos one_lt_two
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
this : 2 * ext i Y ≤ i
⊢ 2 * (2 * y ^ 2) = (2 * y) ^ 2
Tactic:
simp [sq, mul_assoc, mul_left_comm y 2]
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
this : 2 * ext i Y ≤ i
⊢ 2 * y ≤ i
Tactic:
simpa [hYy] using this
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)
⊢ X' ≤ (2 * y ^ 2) ^ 4
Tactic:
have : X' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
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)
this : X' < i ^ 4
⊢ X' ≤ (2 * y ^ 2) ^ 4
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)
this : X' < i ^ 4
⊢ X' ≤ (2 * y ^ 2) ^ 4
Tactic:
exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) (le_trans hi $ by simp) 4)
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)
⊢ X' < i ^ 4
Tactic:
simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
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)
this : X' < i ^ 4
⊢ 0 ≤ i
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)
this : X' < i ^ 4
⊢ 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
⊢ Y' ≤ (2 * y ^ 2) ^ 4
Tactic:
have : Y' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
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
this : Y' < i ^ 4
⊢ Y' ≤ (2 * y ^ 2) ^ 4
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
this : Y' < i ^ 4
⊢ Y' ≤ (2 * y ^ 2) ^ 4
Tactic:
exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) (le_trans hi $ by simp) 4)
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
⊢ Y' < i ^ 4
Tactic:
simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
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
this : Y' < i ^ 4
⊢ 0 ≤ i
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
this : Y' < i ^ 4
⊢ y ^ 2 ≤ 2 * y ^ 2
Tactic:
simp
Proof state after:
no goals