internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ 2 ≤ ext i Y
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

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
ne2 : x✝ ≠ 2
hi : x✝ ≤ y ^ 2
ppi : PPow2 x✝
⊢ 2 ≤ ext x✝ Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_ext_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
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ 2 ≤ ext i Y
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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ 2 ≤ ext i Y

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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ 2 ≤ ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_ext_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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ 2 ≤ ext i Y
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
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ 2 ≤ ext 4 Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_ext_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
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ 2 ≤ ext 4 Y
Tactic:
simp [h₀.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ 2 ≤ ext i Y
Tactic:
have IH : 2 ≤ ext (√i) Y :=
  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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
⊢ 2 ≤ ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
⊢ 2 ≤ ext i Y
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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ 2 ≤ ext i Y

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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 ≤ ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
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_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ 2 ≤ ext i Y
Tactic:
calc
  2 ≤ ext (√i) Y     := IH
  _ ≤ (ext (√i) Y)^2 := by simp
  _ = ext i Y        := by simpa [ppi.sq_sqrt_eq ne2] using Eq.symm heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext (√i) Y ≤ ext (√i) Y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext (√i) Y ^ 2 = ext i Y
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using Eq.symm heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 ≤ ext i Y
Tactic:
calc
  2 ≤ ext (√i) Y         := IH
  _ ≤ (ext (√i) Y)^2     := by simp
  _ ≤ 2 * (ext (√i) Y)^2 := by simp
  _ = ext i Y            := by simpa [ppi.sq_sqrt_eq ne2] using Eq.symm hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext (√i) Y ≤ ext (√i) Y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext (√i) Y ^ 2 ≤ 2 * ext (√i) Y ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.two_le_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 → 2 ≤ ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : 2 ≤ ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext (√i) Y ^ 2 = ext i Y
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using Eq.symm hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ ext i X < ext i Y
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 → ext i X < ext i Y

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 → ext y_1 X < ext y_1 Y
ne2 : x✝ ≠ 2
hi : x✝ ≤ y ^ 2
ppi : PPow2 x✝
⊢ ext x✝ X < ext x✝ Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_ext_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 → ext i X < ext i Y
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ ext i X < ext i Y
Tactic:
by_cases ne4 : 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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : i = 4
⊢ ext i X < ext i Y

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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
⊢ ext i X < ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_ext_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : i = 4
⊢ ext i X < ext i Y
Tactic:
rcases ne4 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 → ext y_1 X < ext y_1 Y
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ ext 4 X < ext 4 Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_ext_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 → ext y_1 X < ext y_1 Y
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ ext 4 X < ext 4 Y
Tactic:
simp [h₀.1, h₀.2, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
⊢ ext i X < ext i Y
Tactic:
have IH : ext (√i) X < ext (√i) Y :=
IH (√i) (sqrt_lt_self_of_one_lt ppi.one_lt) (ppi.sqrt_ne_two ne2 ne4) (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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
⊢ ext i X < ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
⊢ ext i X < ext i Y
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 ne4) (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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext i X < ext i Y

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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i X < ext i Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
⊢ √i ≤ i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext i X < ext i Y
Tactic:
calc
  ext i X = 2 * ext (√i) X := by simpa [ppi.sq_sqrt_eq ne2] using heven.1
  _       < 2 * ext (√i) Y := by simpa using IH
  _       ≤ ext (√i) Y^2   := two_mul_le_sq (two_le_ext_of_seq₀_of_seqₛ h₀ hₛ (ppi.sqrt_ne_two ne2 ne4) (le_trans (by simp) hi) (ppi.sqrt ne2))
  _       = ext i Y        := by simpa [ppi.sq_sqrt_eq ne2] using Eq.symm heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext i X = 2 * ext (√i) X
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using heven.1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ 2 * ext (√i) X < 2 * ext (√i) Y
Tactic:
simpa using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ √i ≤ i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
heven : Seqₛ.Even X Y (√i)
⊢ ext (√i) Y ^ 2 = ext i Y
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using Eq.symm heven.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i X < ext i Y
Tactic:
calc
  ext i X = 2 * ext (√i) X + 1 := by simpa [ppi.sq_sqrt_eq ne2] using hodd.1
  _       < 2 * ext (√i) Y + 1 := by simpa using IH
  _       ≤ 2 * ext (√i) Y^2   := lt_iff_succ_le.mp
    (by simp [sq]; exact lt_mul_self (lt_iff_succ_le.mpr $ by
          simp [one_add_one_eq_two]; exact (two_le_ext_of_seq₀_of_seqₛ h₀ hₛ (ppi.sqrt_ne_two ne2 ne4) (le_trans (by simp) hi) (ppi.sqrt ne2))))
  _       = ext i Y            := by simpa [ppi.sq_sqrt_eq ne2] using Eq.symm hodd.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i X = 2 * ext (√i) X + 1
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using hodd.1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext (√i) X + 1 < 2 * ext (√i) Y + 1
Tactic:
simpa using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 * ext (√i) Y < 2 * ext (√i) Y ^ 2
Tactic:
simp [sq]
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 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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext (√i) Y < ext (√i) Y * ext (√i) Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ ext (√i) Y < ext (√i) Y * ext (√i) Y
Tactic:
exact lt_mul_self (lt_iff_succ_le.mpr $ by
simp [one_add_one_eq_two]; exact (two_le_ext_of_seq₀_of_seqₛ h₀ hₛ (ppi.sqrt_ne_two ne2 ne4) (le_trans (by simp) hi) (ppi.sqrt ne2)))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 1 + 1 ≤ ext (√i) Y
Tactic:
simp [one_add_one_eq_two]
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 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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 ≤ ext (√i) Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ 2 ≤ ext (√i) Y
Tactic:
exact (two_le_ext_of_seq₀_of_seqₛ h₀ hₛ (ppi.sqrt_ne_two ne2 ne4) (le_trans (by simp) hi) (ppi.sqrt ne2))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.ext_le_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 → ext y_1 X < ext y_1 Y
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : ext (√i) X < ext (√i) Y
hodd : Seqₛ.Odd X Y (√i)
⊢ √i ≤ i
Tactic:
simp
Proof state after:
no goals