Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt (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
ne2 : i ≠ 2
⊢ PPow2 (√i)
Tactic:
rcases ppi with ⟨pi, m, _, sppm, him⟩
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
⊢ PPow2 (√i)

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
⊢ PPow2 (√i)
Tactic:
have : LenBit i m ↔ (√i)^2 = i ∧ LenBit (√i) m :=
  sppm.lenbit_iff him.le pi (lt_of_le_of_ne (one_lt_iff_two_le.mp $ sppm.one_lt him) (Ne.symm ne2))
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
⊢ PPow2 (√i)

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
⊢ PPow2 (√i)
Tactic:
rcases this.mp him with ⟨e, H⟩
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
⊢ PPow2 (√i)

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
⊢ PPow2 (√i)
Tactic:
have psqi : Pow2 (√i) := Pow2.sq_iff.mp (by simp [e, pi])
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
⊢ PPow2 (√i)

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
⊢ PPow2 (√i)
Tactic:
have one_lt_sqi : 1 < √i := one_lt_sq_iff.mp (by simpa [e] using sppm.one_lt him)
State after:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ PPow2 (√i)

State before:
case 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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
this : SPPow2 (m % (2 * √i))
⊢ PPow2 (√i)
Tactic:
exact ⟨psqi, m % (2 * √i), mod_lt _ (by simp [psqi.pos]), this, by simp [H]⟩
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
⊢ Pow2 ((√i) ^ 2)
Tactic:
simp [e, pi]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
⊢ 1 < (√i) ^ 2
Tactic:
simpa [e] using sppm.one_lt him
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ ¬LenBit 1 (m % (2 * √i))
Tactic:
simpa [LenBit.mod] using sppm.not_lenbit_one
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ Pow2 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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ Pow2 (2 * √i)
Tactic:
simp [psqi]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ 2 < 2 * √i
Tactic:
simp [one_lt_sqi]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
⊢ ∀ i_1 ≤ m % (2 * √i),
    Pow2 i_1 → 2 < i_1 → (LenBit i_1 (m % (2 * √i)) ↔ (√i_1) ^ 2 = i_1 ∧ LenBit (√i_1) (m % (2 * √i)))
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))
Tactic:
have hjsi : j < 2 * √i := lt_of_le_of_lt hj (mod_lt _ (by simp [psqi.pos]))
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))
Tactic:
have : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m := sppm.lenbit_iff (le_trans hj (by simp)) 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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
⊢ LenBit j (m % (2 * √i)) ↔ (√j) ^ 2 = j ∧ LenBit (√j) (m % (2 * √i))
Tactic:
rw [LenBit.mod_pow2, this] <;> try simp [pj, psqi, hjsi]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
⊢ (√j) ^ 2 = j → (LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i)))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
⊢ (√j) ^ 2 = j → (LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i)))
Tactic:
intro hsqj
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
⊢ LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
⊢ LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i))
Tactic:
have : Pow2 (√j) := pj.sqrt hsqj
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i))

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ LenBit (√j) m ↔ LenBit (√j) (m % (2 * √i))
Tactic:
rw [LenBit.mod_pow2] <;> try simp [psqi, this]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ √j < 2 * √i

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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
⊢ 0 < 2 * √i
Tactic:
simp [psqi.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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
⊢ m % (2 * √i) ≤ m
Tactic:
simp
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
⊢ j < 2 * √i
Tactic:
simp [pj, psqi, hjsi]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ Pow2 (2 * √i)
Tactic:
simp [psqi, this]
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ √j < 2 * √i
Tactic:
exact lt_of_le_of_lt (by simp) hjsi
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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝¹ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
j : M
hj : j ≤ m % (2 * √i)
pj : Pow2 j
lt2 : 2 < j
hjsi : j < 2 * √i
this✝ : LenBit j m ↔ (√j) ^ 2 = j ∧ LenBit (√j) m
hsqj : (√j) ^ 2 = j
this : Pow2 (√j)
⊢ √j ≤ 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
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
this : SPPow2 (m % (2 * √i))
⊢ 0 < 2 * √i
Tactic:
simp [psqi.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 ⊧ₘ* 𝐈𝚫₀
i : M
ne2 : i ≠ 2
pi : Pow2 i
m : M
left✝ : m < 2 * i
sppm : SPPow2 m
him : LenBit i m
this✝ : LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
e : (√i) ^ 2 = i
H : LenBit (√i) m
psqi : Pow2 (√i)
one_lt_sqi : 1 < √i
this : SPPow2 (m % (2 * √i))
⊢ LenBit (√i) (m % (2 * √i))
Tactic:
simp [H]
State after:
no goals