internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof 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)))
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
⊢ PPow2 (i ^ 2)
Tactic:
rcases ppi.exists_spp with ⟨m, hm, sppm, hi⟩
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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))
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ i ^ 2 ≠ 1
Tactic:
simp
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ ¬i = 1
Tactic:
rintro rfl
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
sppm : SPPow2 m
ppi : PPow2 1
hm : m < 2 * 1
hi : LenBit 1 m
⊢ False
Tactic:
exact sppm.not_lenbit_one hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ppi : PPow2 i
m : M
hm : m < 2 * i
sppm : SPPow2 m
hi : LenBit i m
⊢ 2 ≠ i ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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)
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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]
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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)
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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)
Proof 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)