internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hysqi : y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ y < i
Tactic:
simp [←hYy, ppi.pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hysqi : y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
j : M
hj : j ≤ y ^ 2
jne2 : j ≠ 2
ppj : PPow2 j
hjy : ¬j ≤ y
this : Pow2 y
⊢ y < j
Tactic:
simpa using hjy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hysqi : y ^ 2 < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (y ^ 2) X' Y'
⊢ ext (i ^ 2) X' = 2 * x ∧ ext (i ^ 2) Y' = y ^ 2
Tactic:
simp at *
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : ¬i = 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (y ^ 2) X' Y'
hysqi : y < i
⊢ ext (i ^ 2) X' = 2 * x ∧ ext (i ^ 2) Y' = y ^ 2
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : ¬i = 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (y ^ 2) X' Y'
hysqi : y < i
⊢ ext (i ^ 2) X' = 2 * x ∧ ext (i ^ 2) Y' = y ^ 2
Tactic:
rw [ext_append_last, ext_append_last] <;> try simp [hxsqi, hysqi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero
Proof state before:
case hz
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : ¬i = 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hseqₛ' : Seqₛ (y ^ 2) X' Y'
hysqi : y < i
⊢ 2 * x < i ^ 2
Tactic:
simp [hxsqi, hysqi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.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
⊢ (∃ y', y = y' ^ 2 ∧ Exponential x y') → Exponential (2 * x) y
Tactic:
rintro ⟨y, rfl, 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 y
⊢ Exponential (2 * x) (y ^ 2)
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_even
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 y
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
exact bit_zero h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_even_sq
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 ^ 2) → 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 (2 * x) (y ^ 2)
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_even_sq
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 (2 * x) (y ^ 2)
⊢ Exponential x y
Tactic:
rcases exponential_exists_sq_of_exponential_even 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 (2 * x) (y ^ 2)
y' : M
e : y ^ 2 = y' ^ 2
h : Exponential x y'
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_even_sq
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 (2 * x) (y ^ 2)
y' : M
e : y ^ 2 = y' ^ 2
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_even_sq
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 (2 * x) (y ^ 2)
y' : M
e : y ^ 2 = y' ^ 2
h : Exponential x y'
⊢ y = y'
Tactic:
simpa using e
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 + 1) y → ∃ y', y = 2 * 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 + 1 = 0
⊢ ∃ y', 1 = 2 * 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 + 1
hYy : ext i Y = y
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = 2 * x + 1
hYy : ext i Y = y
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x 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 ⊧ₘ* 𝐈𝚫₀
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 + 1
hYy : ext i Y = y
ne4 : i = 4
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'

case neg
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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have : Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i) :=
  hseqₛ (√i) (sqrt_le_of_le_sq hi) (ppi.sqrt_ne_two ne2 ne4) (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 ⊧ₘ* 𝐈𝚫₀
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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
this : Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i)
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
this : Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i)
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
rcases this with (⟨hXi, _⟩ | ⟨hXi, hYi⟩)
Proof state after:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'

case neg.inr.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
hYi : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
hx : 2 * x + 1 = 0
⊢ ∃ y', 1 = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
simp at hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
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 + 1
hYy : ext i Y = y
ne4 : i = 4
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x 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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have ex : x = 0 := by simpa [hseq₀.1] using hXx
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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have ey : y = 2 := by simpa [hseq₀.2] using Eq.symm hYy
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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
ey : y = 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
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 ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
ey : y = 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
exact ⟨1, by simp [ex, ey]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
⊢ x = 0
Tactic:
simpa [hseq₀.1] using hXx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
⊢ y = 2
Tactic:
simpa [hseq₀.2] using Eq.symm hYy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x + 1
hYy : ext 4 Y = y
ex : x = 0
ey : y = 2
⊢ y = 2 * 1 ^ 2 ∧ Exponential x 1
Tactic:
simp [ex, ey]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have hXx : 2 * x + 1 = 2 * ext (√i) X := by simpa [ppi.sq_sqrt_eq ne2, hXx] using hXi
Proof state after:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have : 2 ∣ 2 * x + 1 := by rw [hXx]; simp
Proof state after:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
this : 2 ∣ 2 * x + 1
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
this : 2 ∣ 2 * x + 1
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have : ¬2 ∣ 2 * x + 1 := by simp [←mod_eq_zero_iff_dvd, one_lt_two]
Proof state after:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
this✝ : 2 ∣ 2 * x + 1
this : ¬2 ∣ 2 * x + 1
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case neg.inl.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
this✝ : 2 ∣ 2 * x + 1
this : ¬2 ∣ 2 * x + 1
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = 2 * x + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ 2 * x + 1 = 2 * ext (√i) X
Tactic:
simpa [ppi.sq_sqrt_eq ne2, hXx] using hXi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx✝ : ext i X = 2 * x + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
⊢ 2 ∣ 2 * x + 1
Tactic:
rw [hXx]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx✝ : ext i X = 2 * x + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
⊢ 2 ∣ 2 * ext (√i) X
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx✝ : ext i X = 2 * x + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
⊢ 2 ∣ 2 * ext (√i) X
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx✝ : ext i X = 2 * x + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
right✝ : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : 2 * x + 1 = 2 * ext (√i) X
this : 2 ∣ 2 * x + 1
⊢ ¬2 ∣ 2 * x + 1
Tactic:
simp [←mod_eq_zero_iff_dvd, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_odd
Proof state before:
case neg.inr.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
hYi : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'
Tactic:
have hXx : x = ext (√i) X := by simpa [ppi.sq_sqrt_eq ne2, hXx] using hXi
Proof state after:
case neg.inr.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 + 1
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
hYi : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
hXx : x = ext (√i) X
⊢ ∃ y', y = 2 * y' ^ 2 ∧ Exponential x y'