internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ 2 * y < 2 * (2 * y ^ 2)
Tactic:
simp
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential x y
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ y < 2 * y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ y < 2 * y ^ 2
Tactic:
exact lt_of_lt_of_le this le_two_mul_left
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this : y < y ^ 2
⊢ y ≤ 2 * y
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ
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
H : Exponential (2 * x + 1) (2 * y ^ 2)
IH : ∀ y_1 < 2 * (2 * y ^ 2), ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < 2 * (2 * y ^ 2)
left✝ : 2 * y ^ 2 ≤ 2 * (2 * y ^ 2)
ne1 : ¬y = 1
this✝ : y < y ^ 2
this : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z
⊢ y ≤ 2 * y
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_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 ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ Exponential (x + 1) (2 * y) → Exponential x y
Tactic:
intro h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential (x + 1) (2 * y)
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_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 ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential (x + 1) (2 * y)
⊢ Exponential x y
Tactic:
rcases exponential_succ.mp h with ⟨y', e, h⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h✝ : Exponential (x + 1) (2 * y)
y' : M
e : 2 * y = 2 * y'
h : Exponential x y'
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_two
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h✝ : Exponential (x + 1) (2 * y)
y' : M
e : 2 * y = 2 * y'
h : Exponential x y'
⊢ Exponential x y
Tactic:
simpa [show y = y' from by simpa using e] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_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 ⊧ₘ* 𝐈𝚫₀
x y : M
h✝ : Exponential (x + 1) (2 * y)
y' : M
e : 2 * y = 2 * y'
h : Exponential x y'
⊢ y = y'
Tactic:
simpa using e
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_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 ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ Exponential x y → Exponential (x + 1) (2 * y)
Tactic:
intro h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ Exponential (x + 1) (2 * y)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_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 ⊧ₘ* 𝐈𝚫₀
x y : M
h : Exponential x y
⊢ Exponential (x + 1) (2 * y)
Tactic:
exact exponential_succ.mpr ⟨y, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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
⊢ 1 ≤ ext i X
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 → 1 ≤ ext i X

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

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

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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
hodd : Seqₛ.Odd X Y (√i)
⊢ 1 ≤ ext i X
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
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.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
heven : Seqₛ.Even X Y (√i)
⊢ 1 ≤ ext i X
Tactic:
have : ext i X = 2 * ext (√i) X := by simpa [ppi.sq_sqrt_eq ne2] using heven.1
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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
heven : Seqₛ.Even X Y (√i)
this : ext i X = 2 * ext (√i) X
⊢ 1 ≤ ext i X
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
heven : Seqₛ.Even X Y (√i)
this : ext i X = 2 * ext (√i) X
⊢ 1 ≤ ext i X
Tactic:
exact le_trans IH (by simp [this])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
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.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
heven : Seqₛ.Even X Y (√i)
this : ext i X = 2 * ext (√i) X
⊢ ext (√i) X ≤ ext i X
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
hodd : Seqₛ.Odd X Y (√i)
⊢ 1 ≤ ext i X
Tactic:
have : ext i X = 2 * ext (√i) X + 1 := by simpa [ppi.sq_sqrt_eq ne2] using hodd.1
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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
hodd : Seqₛ.Odd X Y (√i)
this : ext i X = 2 * ext (√i) X + 1
⊢ 1 ≤ ext i X
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
hodd : Seqₛ.Odd X Y (√i)
this : ext i X = 2 * ext (√i) X + 1
⊢ 1 ≤ ext i X
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.one_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 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
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.zero_uniq
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 : M
h : Exponential 0 y
⊢ y = 1
Tactic:
rcases h with (⟨_, rfl⟩ | ⟨X, _, Y, _, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, _⟩⟩)
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 ⊧ₘ* 𝐈𝚫₀
left✝ : 0 = 0
⊢ 1 = 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 ⊧ₘ* 𝐈𝚫₀
y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = 0
right✝ : ext u Y = y
⊢ y = 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq
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 ⊧ₘ* 𝐈𝚫₀
left✝ : 0 = 0
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq
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 ⊧ₘ* 𝐈𝚫₀
y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = 0
right✝ : ext u Y = y
⊢ y = 1
Tactic:
have : 1 ≤ ext u X  := one_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
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 ⊧ₘ* 𝐈𝚫₀
y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = 0
right✝ : ext u Y = y
this : 1 ≤ ext u X
⊢ y = 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq
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 ⊧ₘ* 𝐈𝚫₀
y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = 0
right✝ : ext u Y = y
this : 1 ≤ ext u X
⊢ y = 1
Tactic:
simp [hX] at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq_iff
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 : M
⊢ y = 1 → Exponential 0 y
Tactic:
rintro rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 0 1
Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Exponential 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.succ_lt_s
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 + 1) y
⊢ 2 ≤ y
Tactic:
rcases h with (⟨h, rfl⟩ | ⟨X, _, Y, _, H₀, Hₛ, ⟨u, hu, ne2, ppu, _, hY⟩⟩)
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
h : x + 1 = 0
⊢ 2 ≤ 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 X : M
left✝² : X ≤ y ^ 4
Y : M
left✝¹ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
left✝ : ext u X = x + 1
hY : ext u Y = y
⊢ 2 ≤ y
Theorem: LO.FirstOrder.Arith.Model.Exponential.succ_lt_s
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
h : x + 1 = 0
⊢ 2 ≤ 1
Tactic:
simp at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.succ_lt_s
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
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
left✝ : ext u X = x + 1
hY : ext u Y = y
⊢ 2 ≤ y
Tactic:
simpa [hY] using two_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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₁ y₂ : M
⊢ Exponential x y₁ → Exponential x y₂ → y₁ = y₂
Tactic:
intro h₁ h₂
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
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₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
⊢ y₁ = y₂
Tactic:
wlog h : y₁ ≤ y₂
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {x y₁ y₂ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
h : ¬y₁ ≤ y₂
⊢ y₁ = y₂

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
h : y₁ ≤ y₂
⊢ y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y₁ y₂ : M
h₁ : Exponential x y₁
h₂ : Exponential x y₂
h : y₁ ≤ y₂
⊢ y₁ = y₂
Tactic:
revert x h y₁
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y₂ : M
⊢ ∀ {x y₁ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
Theorem: LO.FirstOrder.Arith.Model.Exponential.uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y₂ : M
⊢ ∀ {x y₁ : M}, Exponential x y₁ → Exponential x y₂ → y₁ ≤ y₂ → y₁ = y₂
Tactic:
suffices ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂ by
  intro x y₁ h₁ h₂ hy; exact this x h₂.lt y₁ hy h₁ h₂
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y₂ : M
⊢ ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂