Theorem: LO.FirstOrder.Arith.Model.PPow2.sq (Arithmetization/ISigmaZero/Exponential/PPow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
⊢ PPow2 (i ^ 2)
Tactic:
rcases ppi.exists_spp with ⟨m, hm, sppm, hi⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ PPow2 (i ^ 2)

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
⊢ PPow2 (i ^ 2)
Tactic:
by_cases ne1 : i = 1
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : i = 1
⊢ PPow2 (i ^ 2)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
⊢ PPow2 (i ^ 2)

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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
⊢ PPow2 (i ^ 2)
Tactic:
have : m < i^2 :=
  lt_of_lt_of_le hm
    (two_mul_le_sq $ one_lt_iff_two_le.mp $ lt_of_le_of_ne (pos_iff_one_le.mp $ ppi.pos) (Ne.symm ne1))
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
this : m < i ^ 2
⊢ PPow2 (i ^ 2)

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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
this : m < i ^ 2
⊢ PPow2 (i ^ 2)
Tactic:
exact ⟨ppi.pow2.sq, m + i^2,
  by simp [two_mul, hm, this],
  sppm', LenBit.add_self 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ ¬LenBit 1 (m + i ^ 2)
Tactic:
rw [LenBit.add_pow2] <;> try simp [ppi.pow2, sppm.not_lenbit_one, sppm.one_lt hi]
State after:
no goals

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ 1 < i ^ 2
Tactic:
simp [ppi.pow2, sppm.not_lenbit_one, sppm.one_lt 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ LenBit 2 (m + i ^ 2)
Tactic:
rw [LenBit.add_pow2] <;> try simp [ppi.pow2, sppm.lenbit_two]
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ 2 < i ^ 2

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ 2 < i ^ 2
Tactic:
exact lt_of_le_of_ne (ppi.pow2.sq.two_le $ by simp; rintro rfl; exact sppm.not_lenbit_one hi) (by simp)
State after:
no goals

State before:
case pj
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ Pow2 (i ^ 2)
Tactic:
simp [ppi.pow2, sppm.lenbit_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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ i ^ 2 ≠ 1
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ ¬i = 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ ¬i = 1
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
sppm : SPPow2 m
ppi : PPow2 1
hm : m < 2 * 1
hi : LenBit 1 m
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
sppm : SPPow2 m
ppi : PPow2 1
hm : m < 2 * 1
hi : LenBit 1 m
⊢ False
Tactic:
exact sppm.not_lenbit_one 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ 2 ≠ i ^ 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ ∀ i_1 ≤ m + i ^ 2, Pow2 i_1 → 2 < i_1 → (LenBit i_1 (m + i ^ 2) ↔ (√i_1) ^ 2 = i_1 ∧ LenBit (√i_1) (m + i ^ 2))
Tactic:
intro j hj pj lt2
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
have hsqi : i < i^2 := lt_square_of_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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
have hmi : m < i^2 := lt_of_lt_of_le hm (two_mul_le_sq $ one_lt_iff_two_le.mp $ sppm.one_lt hi)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ LenBit j (m + i ^ 2) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
rw [LenBit.add_pow2_iff_of_lt] <;> try simp [pj, ppi.pow2, hmi]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
constructor
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m → (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2) → j = i ^ 2 ∨ LenBit j m

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ m < i ^ 2
Tactic:
simp [pj, ppi.pow2, hmi]
State after:
no goals

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m → (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
rintro (rfl | hj)
State after:
case mp.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : i ^ 2 ≤ m + i ^ 2
pj : Pow2 (i ^ 2)
lt2 : 2 < i ^ 2
⊢ (√i ^ 2) ^ 2 = i ^ 2 ∧ LenBit (√i ^ 2) (m + i ^ 2)

case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
case mp.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : i ^ 2 ≤ m + i ^ 2
pj : Pow2 (i ^ 2)
lt2 : 2 < i ^ 2
⊢ (√i ^ 2) ^ 2 = i ^ 2 ∧ LenBit (√i ^ 2) (m + i ^ 2)
Tactic:
simp
State after:
case mp.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : i ^ 2 ≤ m + i ^ 2
pj : Pow2 (i ^ 2)
lt2 : 2 < i ^ 2
⊢ LenBit i (m + i ^ 2)

State before:
case mp.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : i ^ 2 ≤ m + i ^ 2
pj : Pow2 (i ^ 2)
lt2 : 2 < i ^ 2
⊢ LenBit i (m + i ^ 2)
Tactic:
rw [LenBit.add_pow2] <;> simp [hi, ppi.pow2, hsqi]
State after:
no goals

State before:
case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
have : (√j)^2 = j := sppm.sq_sqrt_eq hj pj (ne_of_gt lt2)
State after:
case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
this : (√j) ^ 2 = j
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)

State before:
case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
this : (√j) ^ 2 = j
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2)
Tactic:
rw [LenBit.add_pow2_iff_of_lt] <;> try simp [ppi.pow2, pj.sqrt this, hmi]
State after:
case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
this : (√j) ^ 2 = j
⊢ (√j) ^ 2 = j ∧ (√j = i ^ 2 ∨ LenBit (√j) m)

State before:
case mp.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
this : (√j) ^ 2 = j
⊢ (√j) ^ 2 = j ∧ (√j = i ^ 2 ∨ LenBit (√j) m)
Tactic:
simp [sppm.sqrt hj pj (ne_of_gt lt2), this]
State after:
no goals

State before:
case mp.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj✝ : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
hj : LenBit j m
this : (√j) ^ 2 = j
⊢ m < i ^ 2
Tactic:
simp [ppi.pow2, pj.sqrt this, hmi]
State after:
no goals

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
⊢ (√j) ^ 2 = j ∧ LenBit (√j) (m + i ^ 2) → j = i ^ 2 ∨ LenBit j m
Tactic:
rintro ⟨ej, lb⟩
State after:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ j = i ^ 2 ∨ LenBit j m

State before:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ j = i ^ 2 ∨ LenBit j m
Tactic:
have hsqj : √j < i^2 := lt_of_mul_lt_mul_left (a := 2) (by calc
  2 * √j ≤ (√j)^2  := two_mul_le_sq
                          (one_lt_iff_two_le.mp <| one_lt_sq_iff.mp <| by
                            rw [ej]; exact lt_trans _ _ _ one_lt_two lt2)
  _      ≤ j       := by simp
  _      ≤ m + i^2 := hj
  _      < 2 * i^2 := by simp [two_mul, hmi])
State after:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj : √j < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m

State before:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj : √j < i ^ 2
⊢ j = i ^ 2 ∨ LenBit j m
Tactic:
have hsqj : LenBit (√j) m := (LenBit.add_pow2 (pj.sqrt ej) ppi.pow2.sq hsqj).mp lb
State after:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
⊢ j = i ^ 2 ∨ LenBit j m

State before:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
⊢ j = i ^ 2 ∨ LenBit j m
Tactic:
by_cases hjm : j ≤ m
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : j ≤ m
⊢ j = i ^ 2 ∨ LenBit j m

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
⊢ j = i ^ 2 ∨ LenBit j m

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 2 * √j < 2 * i ^ 2
Tactic:
calc
2 * √j ≤ (√j)^2  := two_mul_le_sq
(one_lt_iff_two_le.mp <| one_lt_sq_iff.mp <| by
rw [ej]; exact lt_trans _ _ _ one_lt_two lt2)
_      ≤ j       := by simp
_      ≤ m + i^2 := hj
_      < 2 * i^2 := by simp [two_mul, hmi]
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 1 < (√j) ^ 2
Tactic:
rw [ej]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 1 < j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 1 < j
Tactic:
exact lt_trans _ _ _ one_lt_two lt2
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ (√j) ^ 2 ≤ j
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ m + i ^ 2 < 2 * i ^ 2
Tactic:
simp [two_mul, hmi]
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : j ≤ m
⊢ j = i ^ 2 ∨ LenBit j m
Tactic:
exact Or.inr <| sppm.of_sqrt pj hjm ej hsqj
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
⊢ j = i ^ 2 ∨ LenBit j m
Tactic:
have : i = √j := sppm.last_uniq ppi.pow2 (pj.sqrt ej) hi hsqj hmi (by simpa [ej] using hjm)
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
this : i = √j
⊢ j = i ^ 2 ∨ LenBit j m

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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
this : i = √j
⊢ j = i ^ 2 ∨ LenBit j m
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
this : i = √j
⊢ j = i ^ 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
this : i = √j
⊢ j = i ^ 2
Tactic:
simp [this, ej]
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
j : M
hj : j ≤ m + i ^ 2
pj : Pow2 j
lt2 : 2 < j
hsqi : i < i ^ 2
hmi : m < i ^ 2
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
hsqj✝ : √j < i ^ 2
hsqj : LenBit (√j) m
hjm : ¬j ≤ m
⊢ m < (√j) ^ 2
Tactic:
simpa [ej] using hjm
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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : i = 1
⊢ PPow2 (i ^ 2)
Tactic:
rcases ne1
State after:
case pos.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
sppm : SPPow2 m
ppi : PPow2 1
hm : m < 2 * 1
hi : LenBit 1 m
sppm' : SPPow2 (m + 1 ^ 2)
⊢ PPow2 (1 ^ 2)

State before:
case pos.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
sppm : SPPow2 m
ppi : PPow2 1
hm : m < 2 * 1
hi : LenBit 1 m
sppm' : SPPow2 (m + 1 ^ 2)
⊢ PPow2 (1 ^ 2)
Tactic:
simpa using 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 ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
this : m < i ^ 2
⊢ m + i ^ 2 < 2 * i ^ 2
Tactic:
simp [two_mul, hm, this]
State after:
no goals