internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof state before:
case inl.h.hij
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ j ^ 2 < i ^ 2
Tactic:
simp [ppi.sq, ppj.sq, lt_of_le_of_lt hj hz, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2 ∨
    ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
      ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2
Tactic:
right
Proof state after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
    ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof state before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) + 1 ∧
    ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = 2 * ext j (Exponential.append (i ^ 2) Y y) ^ 2
Tactic:
rw [ext_append_of_lt, ext_append_of_lt, ext_append_of_lt, ext_append_of_lt] <;> try simp [ppi.sq, ppj.sq, lt_of_le_of_lt hj hz, *]
Proof state after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) X = 2 * ext j X + 1 ∧ ext (j ^ 2) Y = 2 * ext j Y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof state before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ ext (j ^ 2) X = 2 * ext j X + 1 ∧ ext (j ^ 2) Y = 2 * ext j Y ^ 2
Tactic:
exact H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.append
Proof state before:
case inr.h.hij
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Odd X Y j
⊢ j ^ 2 < i ^ 2
Tactic:
simp [ppi.sq, ppj.sq, lt_of_le_of_lt hj hz, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_zero_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 ⊧ₘ* 𝐈𝚫₀
⊢ 0 = 0 ∧ 1 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≤ 2 ^ 4
Tactic:
simp [pow_four_eq_sq_sq, two_pow_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 * 4 ≤ 2 ^ 4
Tactic:
simp [pow_four_eq_sq_sq, two_pow_two_eq_four, sq (4 : M)]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 ≤ 4
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 ≤ 4
Tactic:
exact le_of_lt two_lt_four
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Seq₀ 4 (2 * 4)
Tactic:
simp [Seq₀, ext, one_lt_four, two_lt_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Seqₛ 2 4 (2 * 4)
Tactic:
simp [Seqₛ]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∀ u ≤ 2, ¬u = 2 → PPow2 u → Seqₛ.Even 4 (2 * 4) u ∨ Seqₛ.Odd 4 (2 * 4) u
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∀ u ≤ 2, ¬u = 2 → PPow2 u → Seqₛ.Even 4 (2 * 4) u ∨ Seqₛ.Odd 4 (2 * 4) u
Tactic:
intro i hi ne2 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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : i ≤ 2
ne2 : ¬i = 2
ppi : PPow2 i
⊢ Seqₛ.Even 4 (2 * 4) i ∨ Seqₛ.Odd 4 (2 * 4) i
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
hi : i ≤ 2
ne2 : ¬i = 2
ppi : PPow2 i
⊢ Seqₛ.Even 4 (2 * 4) i ∨ Seqₛ.Odd 4 (2 * 4) i
Tactic:
exact False.elim <| not_le.mpr (ppi.two_lt ne2) hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≤ 2 ^ 2
Tactic:
simp [two_pow_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≠ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ PPow2 4 ∧ ext 4 4 = 1 ∧ ext 4 (2 * 4) = 2
Tactic:
simp [ext, one_lt_four, two_lt_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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
⊢ Pow2 (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 → Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : x✝ ≠ 2
hi : x✝ ≤ y ^ 2
ppi : PPow2 x✝
⊢ Pow2 (ext x✝ Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext i Y)
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ Pow2 (ext i Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ Pow2 (ext 4 Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ Pow2 (ext 4 Y)
Tactic:
simp [h₀.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ Pow2 (ext i Y)
Tactic:
have ppsq : Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
⊢ Pow2 (ext i Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
⊢ Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
⊢ Pow2 (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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
⊢ Pow2 (ext i Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (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.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
⊢ Pow2 (ext i Y)
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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Tactic:
simp [this, ppsq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
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.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
⊢ Pow2 (ext i Y)
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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Tactic:
simp [this, ppsq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_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 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
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.range_pow2
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 x y
⊢ Pow2 y
Tactic:
rcases h with (⟨rfl, rfl⟩ | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, rfl, 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 ⊧ₘ* 𝐈𝚫₀
⊢ Pow2 1

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 : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ Pow2 (ext u Y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_pow2
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 ⊧ₘ* 𝐈𝚫₀
⊢ Pow2 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.range_pow2
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 : M
H₀ : Seq₀ X Y
u : M
ne2 : u ≠ 2
ppu : PPow2 u
bX : X ≤ ext u Y ^ 4
bY : Y ≤ ext u Y ^ 4
Hₛ : Seqₛ (ext u Y) X Y
hu : u ≤ ext u Y ^ 2
⊢ Pow2 (ext u Y)
Tactic:
exact pow2_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
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
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ i ≤ ext i Y ^ 2
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 → i ≤ ext i Y ^ 2

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

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