internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
⊢ i ≤ ext i Y ^ 2
Tactic:
rcases show Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i) from
  hₛ (√i) (sqrt_le_of_le_sq $ hi) (ppi.sqrt_ne_two ne2 ei) (ppi.sqrt ne2) with (heven | hodd)
Proof state after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
⊢ i ≤ ext i Y ^ 2

case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ √i ≤ i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
⊢ i ≤ ext i Y ^ 2
Tactic:
have : ext i Y = (ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using heven.2
Proof state after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ i ≤ ext i Y ^ 2
Tactic:
have : √i ≤ ext i Y := by simpa [this] using IH
Proof state after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
this✝ : ext i Y = ext (√i) Y ^ 2
this : √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
this✝ : ext i Y = ext (√i) Y ^ 2
this : √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using sq_le_sq.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
⊢ ext i Y = ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ √i ≤ ext i Y
Tactic:
simpa [this] using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
⊢ i ≤ ext i Y ^ 2
Tactic:
have : ext i Y = 2*(ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using hodd.2
Proof state after:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ i ≤ ext i Y ^ 2
Tactic:
have : 2 * √i ≤ ext i Y := by simpa [this] using mul_le_mul_left (a := 2) IH
Proof state after:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝ : ext i Y = 2 * ext (√i) Y ^ 2
this : 2 * √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝ : ext i Y = 2 * ext (√i) Y ^ 2
this : 2 * √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Tactic:
have : √i ≤ ext i Y := le_trans (le_mul_of_pos_left $ by simp) this
Proof state after:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝¹ : ext i Y = 2 * ext (√i) Y ^ 2
this✝ : 2 * √i ≤ ext i Y
this : √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝¹ : ext i Y = 2 * ext (√i) Y ^ 2
this✝ : 2 * √i ≤ ext i Y
this : √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using sq_le_sq.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i Y = 2 * ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ 2 * √i ≤ ext i Y
Tactic:
simpa [this] using mul_le_mul_left (a := 2) IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.le_sq_ext_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝ : ext i Y = 2 * ext (√i) Y ^ 2
this : 2 * √i ≤ ext i Y
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ 2 * ext i Y ≤ i
Tactic:
induction i using order_induction_iSigmaZero
Proof state after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
⊢ 𝚺₀-Predicate fun {i} => i ≠ 2 → i ≤ y ^ 2 → PPow2 i → 2 * ext i Y ≤ i

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
x✝ : M
a✝ : ∀ y_1 < x✝, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : x✝ ≠ 2
hi : x✝ ≤ y ^ 2
ppi : PPow2 x✝
⊢ 2 * ext x✝ Y ≤ x✝
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
Proof state before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
⊢ 𝚺₀-Predicate fun {i} => i ≠ 2 → i ≤ y ^ 2 → PPow2 i → 2 * ext i Y ≤ i
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ 2 * ext i Y ≤ i
Tactic:
by_cases ei : i = 4
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ 2 * ext i Y ≤ i

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ 2 * ext i Y ≤ i
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ 2 * ext i Y ≤ i
Tactic:
rcases ei with rfl
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
IH : ∀ y_1 < 4, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ 2 * ext 4 Y ≤ 4
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
IH : ∀ y_1 < 4, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ 2 * ext 4 Y ≤ 4
Tactic:
simp [h₀.2, two_mul_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ 2 * ext i Y ≤ i
Tactic:
have IH : 2 * ext (√i) Y ≤ √i :=
  IH (√i) (sqrt_lt_self_of_one_lt ppi.one_lt) (ppi.sqrt_ne_two ne2 ei) (le_trans (by simp) hi) (ppi.sqrt ne2)
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
⊢ 2 * ext i Y ≤ i
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
⊢ 2 * ext i Y ≤ i
Tactic:
rcases show Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i) from
  hₛ (√i) (sqrt_le_of_le_sq $ hi) (ppi.sqrt_ne_two ne2 ei) (ppi.sqrt ne2) with (heven | hodd)
Proof state after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
⊢ 2 * ext i Y ≤ i

case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext i Y ≤ i
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ √i ≤ i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
Proof state before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
⊢ 2 * ext i Y ≤ i
Tactic:
have : ext i Y = (ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using heven.2
Proof state after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ 2 * ext i Y ≤ i
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
Proof state before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ 2 * ext i Y ≤ i
Tactic:
calc
  2 * ext i Y ≤ 2 * (2 * ext i Y)  := le_mul_of_pos_left (by simp)
  _           = (2 * ext (√i) Y)^2 := by simp [this, sq, mul_left_comm, mul_assoc]
  _           ≤ (√i)^2             := sq_le_sq.mpr IH
  _           = i                  := ppi.sq_sqrt_eq ne2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
⊢ ext i Y = ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ 2 * (2 * ext i Y) = (2 * ext (√i) Y) ^ 2
Tactic:
simp [this, sq, mul_left_comm, mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext i Y ≤ i
Tactic:
have : ext i Y = 2*(ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using hodd.2
Proof state after:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ 2 * ext i Y ≤ i
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
Proof state before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ 2 * ext i Y ≤ i
Tactic:
calc
  2 * ext i Y = (2 * ext (√i) Y)^2 := by simp [this, sq, mul_left_comm, mul_assoc]
  _           ≤ (√i)^2             := sq_le_sq.mpr IH
  _           = i                  := ppi.sq_sqrt_eq ne2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i Y = 2 * ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
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 X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 2 * ext y_1 Y ≤ y_1
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 * ext (√i) Y ≤ √i
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ 2 * ext i Y = (2 * ext (√i) Y) ^ 2
Tactic:
simp [this, sq, mul_left_comm, mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_even
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) y → ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
rintro (⟨hx, rfl⟩ | ⟨X, _, Y, _, hseq₀, hseqₛ, i, hi, ne2, ppi, hXx, hYy⟩)
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 ⊧ₘ* 𝐈𝚫₀
x : M
hx : 2 * x = 0
⊢ ∃ y', 1 = y' ^ 2 ∧ Exponential x y'

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 = 2 * x
hYy : ext i Y = y
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'