Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_exists_sq_of_exponential_even (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ Exponential (2 * x) y → ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
rintro (⟨hx, rfl⟩ | ⟨X, _, Y, _, hseq₀, hseqₛ, i, hi, ne2, ppi, hXx, hYy⟩)
State after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
hx : 2 * x = 0
⊢ ∃ y', 1 = y' ^ 2 ∧ Exponential x y'

case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = 2 * x
hYy : ext i Y = y
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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

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
hYy : ext i Y = y
ne4 : ¬i = 4
⊢ ∃ y', y = 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)
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
hYy : ext i Y = y
ne4 : ¬i = 4
this : Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i)
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext i Y = y
ne4 : ¬i = 4
this : Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i)
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
rcases this with (⟨hXi, hYi⟩ | ⟨hXi, _⟩)
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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ ∃ y', y = 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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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 = 0
⊢ ∃ y', 1 = y' ^ 2 ∧ Exponential x y'
Tactic:
exact ⟨1, by simp [show x = 0 from by simpa using hx]⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
hx : 2 * x = 0
⊢ 1 = 1 ^ 2 ∧ Exponential x 1
Tactic:
simp [show x = 0 from by simpa using hx]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
hx : 2 * x = 0
⊢ x = 0
Tactic:
simpa using hx
State after:
no goals

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
hYy : ext i Y = y
ne4 : i = 4
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
rcases ne4 with rfl
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
hYy : ext 4 Y = y
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext 4 Y = y
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have ex : 1 = 2 * x := by simpa [hseq₀.1] using hXx
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
hYy : ext 4 Y = y
ex : 1 = 2 * x
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have : (2 : M) ∣ 1 := by rw [ex]; simp
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
hYy : ext 4 Y = y
ex : 1 = 2 * x
this : 2 ∣ 1
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
this : 2 ∣ 1
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have : ¬(2 : M) ∣ 1 := not_dvd_of_lt (by simp) one_lt_two
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
hYy : ext 4 Y = y
ex : 1 = 2 * x
this✝ : 2 ∣ 1
this : ¬2 ∣ 1
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
this✝ : 2 ∣ 1
this : ¬2 ∣ 1
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
contradiction
State after:
no goals

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
hYy : ext 4 Y = y
⊢ 1 = 2 * x
Tactic:
simpa [hseq₀.1] using hXx
State after:
no goals

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
⊢ 2 ∣ 1
Tactic:
rw [ex]
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
hi : 4 ≤ y ^ 2
ne2 : 4 ≠ 2
ppi : PPow2 4
hXx : ext 4 X = 2 * x
hYy : ext 4 Y = y
ex : 1 = 2 * x
⊢ 2 ∣ 2 * x

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
⊢ 2 ∣ 2 * x
Tactic:
simp
State after:
no goals

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
hYy : ext 4 Y = y
ex : 1 = 2 * x
this : 2 ∣ 1
⊢ 0 < 1
Tactic:
simp
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have hXx : x = ext (√i) X := by simpa [ppi.sq_sqrt_eq ne2, hXx] using hXi
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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have hYy : y = (ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2, hYy] using hYi
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
let X' := X % i
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
let Y' := Y % i
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have bX' : X' ≤ (ext (√i) Y)^4 := by simp [pow_four_eq_sq_sq, ←hYy]; exact le_trans (le_of_lt $ by simp [X', ppi.pos]) hi
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have bY' : Y' ≤ (ext (√i) Y)^4 := by simp [pow_four_eq_sq_sq, ←hYy]; exact le_trans (le_of_lt $ by simp [Y', ppi.pos]) hi
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have hseqₛ' : Seqₛ (ext (√i) Y) X' Y' :=
  hseqₛ.rem ppi (sq_lt_of_lt_sqrt $ ext_lt Y (ppi.sqrt ne2).pos) (by simp [hYy])
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have hseqₘ' : Seqₘ x (ext (√i) Y) X' Y' :=
  ⟨√i, sqrt_le_of_le_sq $ by simp [←hYy, hi], ppi.sqrt_ne_two ne2 ne4, ppi.sqrt ne2,
   by have : √i < i := sqrt_lt_self_of_one_lt ppi.one_lt
      simp [X', Y', this, ext_rem, ppi, ppi.sqrt ne2, hXx]⟩
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
hseqₘ' : Seqₘ x (ext (√i) Y) X' Y'
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
hseqₘ' : Seqₘ x (ext (√i) Y) X' Y'
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have : Exponential x (ext (√i) Y) :=
  Or.inr ⟨X', bX', Y', bY', hseq₀.rem ppi (ppi.four_lt ne2 ne4), hseqₛ', hseqₘ'⟩
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
hseqₘ' : Seqₘ x (ext (√i) Y) X' Y'
this : Exponential x (ext (√i) Y)
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
hseqₘ' : Seqₘ x (ext (√i) Y) X' Y'
this : Exponential x (ext (√i) Y)
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
exact ⟨ext (√i) Y, hYy, this⟩
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
⊢ x = ext (√i) X
Tactic:
simpa [ppi.sq_sqrt_eq ne2, hXx] using hXi
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
⊢ y = ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2, hYy] using hYi
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ X' ≤ ext (√i) Y ^ 4
Tactic:
simp [pow_four_eq_sq_sq, ←hYy]
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ X' ≤ y ^ 2

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ X' ≤ y ^ 2
Tactic:
exact le_trans (le_of_lt $ by simp [X', ppi.pos]) hi
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
⊢ X' < i
Tactic:
simp [X', ppi.pos]
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ Y' ≤ ext (√i) Y ^ 4
Tactic:
simp [pow_four_eq_sq_sq, ←hYy]
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ Y' ≤ y ^ 2

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ Y' ≤ y ^ 2
Tactic:
exact le_trans (le_of_lt $ by simp [Y', ppi.pos]) hi
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
⊢ Y' < i
Tactic:
simp [Y', ppi.pos]
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
⊢ ext (√i) Y ≤ y
Tactic:
simp [hYy]
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
⊢ i ≤ (ext (√i) Y ^ 2) ^ 2
Tactic:
simp [←hYy, hi]
State after:
no goals

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
⊢ ext (√i) X' = x ∧ ext (√i) Y' = ext (√i) Y
Tactic:
have : √i < i := sqrt_lt_self_of_one_lt ppi.one_lt
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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
this : √i < i
⊢ ext (√i) X' = x ∧ ext (√i) Y' = ext (√i) Y

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
hYy✝ : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X
hYi : ext ((√i) ^ 2) Y = ext (√i) Y ^ 2
hXx : x = ext (√i) X
hYy : y = ext (√i) Y ^ 2
X' : M := X % i
Y' : M := Y % i
bX' : X' ≤ ext (√i) Y ^ 4
bY' : Y' ≤ ext (√i) Y ^ 4
hseqₛ' : Seqₛ (ext (√i) Y) X' Y'
this : √i < i
⊢ ext (√i) X' = x ∧ ext (√i) Y' = ext (√i) Y
Tactic:
simp [X', Y', this, ext_rem, ppi, ppi.sqrt ne2, hXx]
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have : 2 ∣ ext i X := by simp [hXx]
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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this : 2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this : 2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
have : ¬2 ∣ ext i X := by
  simp [show ext i X = 2 * ext (√i) X + 1 from by simpa [ppi.sq_sqrt_eq ne2] using hXi,
    ←mod_eq_zero_iff_dvd, one_lt_two]
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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this✝ : 2 ∣ ext i X
this : ¬2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this✝ : 2 ∣ ext i X
this : ¬2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
Tactic:
contradiction
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
⊢ 2 ∣ ext i X
Tactic:
simp [hXx]
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this : 2 ∣ ext i X
⊢ ¬2 ∣ ext i X
Tactic:
simp [show ext i X = 2 * ext (√i) X + 1 from by simpa [ppi.sq_sqrt_eq ne2] using hXi,
  ←mod_eq_zero_iff_dvd, one_lt_two]
State after:
no goals

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
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this : 2 ∣ ext i X
⊢ ext i X = 2 * ext (√i) X + 1
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using hXi
State after:
no goals