Theorem: LO.FirstOrder.Arith.Model.Exponential.bit_zero (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 x y → Exponential (2 * x) (y ^ 2)
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 : x = 0
⊢ Exponential (2 * x) (1 ^ 2)

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 = x
hYy : ext i Y = y
⊢ Exponential (2 * x) (y ^ 2)

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 = x
hYy : ext i Y = y
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have hxsqi : 2 * x < i ^ 2 := lt_of_lt_of_le (by simp [←hXx, ppi.pos]) (two_mul_le_sq ppi.two_le)
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 ⊧ₘ* 𝐈𝚫₀
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
⊢ Exponential (2 * x) (y ^ 2)

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 = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have hysqi : y ^ 2 < i ^ 2 := sq_lt_sq.mpr $ by simp [←hYy, ppi.pos]
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 ⊧ₘ* 𝐈𝚫₀
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
⊢ Exponential (2 * x) (y ^ 2)

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 = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hysqi : y ^ 2 < i ^ 2
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have hiisq : i < i^2 := lt_square_of_lt ppi.one_lt
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 ⊧ₘ* 𝐈𝚫₀
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
⊢ Exponential (2 * x) (y ^ 2)

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 = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hysqi : y ^ 2 < i ^ 2
hiisq : i < i ^ 2
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
let X' := append (i^2) X (2 * x)
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 ⊧ₘ* 𝐈𝚫₀
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)
⊢ Exponential (2 * x) (y ^ 2)

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 = 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)
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
let Y' := append (i^2) Y (y ^ 2)
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 ⊧ₘ* 𝐈𝚫₀
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)
⊢ Exponential (2 * x) (y ^ 2)

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 = 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)
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have bX' : X' ≤ (y^2)^4 := by
  have : X' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
  exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) hi 4)
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 ⊧ₘ* 𝐈𝚫₀
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
⊢ Exponential (2 * x) (y ^ 2)

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 = 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
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have bY' : Y' ≤ (y^2)^4 := by
  have : Y' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
  exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) hi 4)
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 ⊧ₘ* 𝐈𝚫₀
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
⊢ Exponential (2 * x) (y ^ 2)

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 = 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
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have hseq₀' : Seq₀ X' Y' := hseq₀.append ppi.sq (ppi.sq.four_lt ppi.sq_ne_two (ppi.sq_ne_four ne2))
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 ⊧ₘ* 𝐈𝚫₀
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'
⊢ Exponential (2 * x) (y ^ 2)

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 = 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'
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
have hseqₘ' : Seqₘ (2 * x) (y ^ 2) X' Y' :=
  ⟨i ^ 2, sq_le_sq.mpr hi, ppi.sq_ne_two, ppi.sq,
   by simp at *; rw [ext_append_last, ext_append_last] <;> try simp [hxsqi, hysqi]⟩
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 ⊧ₘ* 𝐈𝚫₀
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'
hseqₘ' : Seqₘ (2 * x) (y ^ 2) X' Y'
⊢ Exponential (2 * x) (y ^ 2)

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 = 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'
hseqₘ' : Seqₘ (2 * x) (y ^ 2) X' Y'
⊢ Exponential (2 * x) (y ^ 2)
Tactic:
exact Or.inr <| ⟨X', bX', Y', bY', hseq₀', hseqₛ', hseqₘ'⟩
State after:
no goals

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 : x = 0
⊢ Exponential (2 * x) (1 ^ 2)
Tactic:
rcases hx with rfl
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 ⊧ₘ* 𝐈𝚫₀
⊢ Exponential (2 * 0) (1 ^ 2)

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 ⊧ₘ* 𝐈𝚫₀
⊢ Exponential (2 * 0) (1 ^ 2)
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
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = x
hYy : ext i Y = y
⊢ 2 * x < 2 * i
Tactic:
simp [←hXx, 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 = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
⊢ y < i
Tactic:
simp [←hYy, 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 = 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)
⊢ X' ≤ (y ^ 2) ^ 4
Tactic:
have : X' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
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
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)
this : X' < i ^ 4
⊢ X' ≤ (y ^ 2) ^ 4

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)
this : X' < i ^ 4
⊢ X' ≤ (y ^ 2) ^ 4
Tactic:
exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) hi 4)
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 = 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)
⊢ X' < i ^ 4
Tactic:
simpa [pow_four_eq_sq_sq] using append_lt (i^2) X hxsqi
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 = 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)
this : X' < i ^ 4
⊢ 0 ≤ i
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
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
⊢ Y' ≤ (y ^ 2) ^ 4
Tactic:
have : Y' < i^4 := by simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
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
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
this : Y' < i ^ 4
⊢ Y' ≤ (y ^ 2) ^ 4

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
this : Y' < i ^ 4
⊢ Y' ≤ (y ^ 2) ^ 4
Tactic:
exact le_trans (le_of_lt this) (pow_le_pow_left (by simp) hi 4)
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 = 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
⊢ Y' < i ^ 4
Tactic:
simpa [pow_four_eq_sq_sq] using append_lt (i^2) Y hysqi
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 = 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
this : Y' < i ^ 4
⊢ 0 ≤ i
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
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'
⊢ Seqₛ (y ^ 2) X' Y'
Tactic:
intro j hj jne2 ppj
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
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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
by_cases hjy : j ≤ y
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 = 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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

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 = 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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

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 = 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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
have : Seqₛ y X' Y' := hseqₛ.append ppi (by simp [←hYy, ppi.pos])
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 = 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 : Seqₛ y X' Y'
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

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 = 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 : Seqₛ y X' Y'
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
exact this j hjy jne2 ppj
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 = 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
⊢ y < i
Tactic:
simp [←hYy, ppi.pos]
State after:
no goals

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 = 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
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
have : i = j := by
  have : Pow2 y := by simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
  exact PPow2.sq_uniq this ppi ppj
    ⟨by simp [←hYy, ppi.pos], hi⟩ ⟨by simpa using hjy, hj⟩
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 = 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 : i = j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j

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 = 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 : i = j
⊢ Seqₛ.Even X' Y' j ∨ Seqₛ.Odd X' Y' j
Tactic:
rcases this with rfl
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 = 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'
hj : i ≤ y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i ∨ Seqₛ.Odd X' Y' i

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 = 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'
hj : i ≤ y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i ∨ Seqₛ.Odd X' Y' i
Tactic:
left
State after:
case neg.h
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'
hj : i ≤ y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i

State before:
case neg.h
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'
hj : i ≤ y ^ 2
jne2 : i ≠ 2
ppj : PPow2 i
hjy : ¬i ≤ y
⊢ Seqₛ.Even X' Y' i
Tactic:
simp [Seqₛ.Even] at*
State after:
case neg.h
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'
hj : i ≤ y ^ 2
jne2 : ¬i = 2
ppj : PPow2 i
hysqi : y < i
hjy : y < i
⊢ ext (i ^ 2) X' = 2 * ext i X' ∧ ext (i ^ 2) Y' = ext i Y' ^ 2

State before:
case neg.h
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'
hj : i ≤ y ^ 2
jne2 : ¬i = 2
ppj : PPow2 i
hysqi : y < i
hjy : y < i
⊢ ext (i ^ 2) X' = 2 * ext i X' ∧ ext (i ^ 2) Y' = ext i Y' ^ 2
Tactic:
rw [ext_append_last, ext_append_last, ext_append_of_lt , ext_append_of_lt] <;>
  simp [ppi, ppi.sq, hxsqi, hysqi, hiisq, hXx, 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 = 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
⊢ i = j
Tactic:
have : Pow2 y := by simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
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
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
⊢ i = j

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
⊢ i = j
Tactic:
exact PPow2.sq_uniq this ppi ppj
  ⟨by simp [←hYy, ppi.pos], hi⟩ ⟨by simpa using hjy, hj⟩
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 = 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
⊢ Pow2 y
Tactic:
simpa [hYy] using pow2_ext_of_seq₀_of_seqₛ hseq₀ hseqₛ ne2 hi ppi
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 = 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]
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 = 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
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 = 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 *
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

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]
State after:
no goals

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]
State after:
no goals