internlm/Lean-Github huggingface dataset:
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
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]
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 ∧ (√j = i ^ 2 ∨ LenBit (√j) m)
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
this : (√j) ^ 2 = j
⊢ (√j) ^ 2 = j ∧ (√j = i ^ 2 ∨ LenBit (√j) m)
Tactic:
simp [sppm.sqrt hj pj (ne_of_gt lt2), this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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])
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
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
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
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
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]
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
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]
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
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 1 < j
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
ej : (√j) ^ 2 = j
lb : LenBit (√j) (m + i ^ 2)
⊢ 1 < j
Tactic:
exact lt_trans _ _ _ one_lt_two lt2
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
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
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
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
Proof state after:
no goals
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
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)
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
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
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
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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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]
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
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq
Proof 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
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
sppm' : SPPow2 (m + i ^ 2)
ne1 : ¬i = 1
this : m < i ^ 2
⊢ m + i ^ 2 < 2 * i ^ 2
Tactic:
simp [two_mul, hm, this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ Pow2 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 < 2 * 2 ∧ SPPow2 2 ∧ LenBit 2 2
Tactic:
simp [one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ¬PPow2 0
Tactic:
intro h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : PPow2 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : PPow2 0
⊢ False
Tactic:
simpa using h.pow2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ¬PPow2 1
Tactic:
rintro ⟨_, m, hm, H, _⟩
Proof 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 ⊧ₘ* 𝐈𝚫₀
left✝ : Pow2 1
m : M
hm : m < 2 * 1
H : SPPow2 m
right✝ : LenBit 1 m
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_one
Proof 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 ⊧ₘ* 𝐈𝚫₀
left✝ : Pow2 1
m : M
hm : m < 2 * 1
H : SPPow2 m
right✝ : LenBit 1 m
⊢ False
Tactic:
have : m ≤ 1 := lt_two_iff_le_one.mp (by simpa using hm)
Proof 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 ⊧ₘ* 𝐈𝚫₀
left✝ : Pow2 1
m : M
hm : m < 2 * 1
H : SPPow2 m
right✝ : LenBit 1 m
this : m ≤ 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_one
Proof 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 ⊧ₘ* 𝐈𝚫₀
left✝ : Pow2 1
m : M
hm : m < 2 * 1
H : SPPow2 m
right✝ : LenBit 1 m
this : m ≤ 1
⊢ False
Tactic:
rcases le_one_iff_eq_zero_or_one.mp this with (rfl | rfl) <;> simp at H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
left✝ : Pow2 1
m : M
hm : m < 2 * 1
H : SPPow2 m
right✝ : LenBit 1 m
⊢ m < 2
Tactic:
simpa using hm
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
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
⊢ PPow2 i ↔ i = 2 ∨ ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
by_cases ei : i = 2
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
ei : i = 2
⊢ PPow2 i ↔ i = 2 ∨ ∃ b, i = b ^ 2 ∧ PPow2 b

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
ei : ¬i = 2
⊢ PPow2 i ↔ i = 2 ∨ ∃ b, i = b ^ 2 ∧ PPow2 b
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof 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
ei : i = 2
⊢ PPow2 i ↔ i = 2 ∨ ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
rcases ei with rfl
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 ⊧ₘ* 𝐈𝚫₀
⊢ PPow2 2 ↔ 2 = 2 ∨ ∃ b, 2 = b ^ 2 ∧ PPow2 b
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof 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 ⊧ₘ* 𝐈𝚫₀
⊢ PPow2 2 ↔ 2 = 2 ∨ ∃ b, 2 = b ^ 2 ∧ PPow2 b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
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
ei : ¬i = 2
⊢ PPow2 i ↔ i = 2 ∨ ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
simp [ei]
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
ei : ¬i = 2
⊢ PPow2 i ↔ ∃ b, i = b ^ 2 ∧ PPow2 b
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
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
ei : ¬i = 2
⊢ PPow2 i ↔ ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
constructor
Proof state after:
case neg.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
⊢ PPow2 i → ∃ b, i = b ^ 2 ∧ PPow2 b

case neg.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
⊢ (∃ b, i = b ^ 2 ∧ PPow2 b) → PPow2 i
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof state before:
case neg.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
⊢ PPow2 i → ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
rintro ppi
Proof state after:
case neg.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
ppi : PPow2 i
⊢ ∃ b, i = b ^ 2 ∧ PPow2 b
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof state before:
case neg.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
ppi : PPow2 i
⊢ ∃ b, i = b ^ 2 ∧ PPow2 b
Tactic:
exact ⟨√i, Eq.symm <| ppi.sq_sqrt_eq ei, ppi.sqrt ei⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof state before:
case neg.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
⊢ (∃ b, i = b ^ 2 ∧ PPow2 b) → PPow2 i
Tactic:
rintro ⟨j, rfl, ppj⟩
Proof state after:
case neg.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
j : M
ppj : PPow2 j
ei : ¬j ^ 2 = 2
⊢ PPow2 (j ^ 2)
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim
Proof state before:
case neg.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
j : M
ppj : PPow2 j
ei : ¬j ^ 2 = 2
⊢ PPow2 (j ^ 2)
Tactic:
exact ppj.sq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim'
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
⊢ PPow2 i ↔ i = 2 ∨ 2 < i ∧ ∃ j, i = j ^ 2 ∧ PPow2 j
Tactic:
by_cases ha : 2 < i <;> simp [ha, ←elim]
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
ha : ¬2 < i
⊢ PPow2 i ↔ i = 2
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim'
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
ha : ¬2 < i
⊢ PPow2 i ↔ i = 2
Tactic:
have : i = 0 ∨ i = 1 ∨ i = 2 := by simpa [le_two_iff_eq_zero_or_one_or_two] using ha
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
ha : ¬2 < i
this : i = 0 ∨ i = 1 ∨ i = 2
⊢ PPow2 i ↔ i = 2
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim'
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
ha : ¬2 < i
this : i = 0 ∨ i = 1 ∨ i = 2
⊢ PPow2 i ↔ i = 2
Tactic:
rcases this with (rfl | rfl | rfl) <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.elim'
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
ha : ¬2 < i
⊢ i = 0 ∨ i = 1 ∨ i = 2
Tactic:
simpa [le_two_iff_eq_zero_or_one_or_two] using ha
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 4 = 2 ^ 2 ∧ PPow2 2
Tactic:
simp [two_pow_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_le
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
hi : PPow2 i
⊢ 2 ≤ i
Tactic:
simp [←one_add_one_eq_two, ←lt_iff_succ_le, hi.one_lt]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ¬PPow2 3
Tactic:
intro h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : PPow2 3
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : PPow2 3
⊢ False
Tactic:
simpa [sqrt_three] using h.sqrt (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : PPow2 3
⊢ 3 ≠ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_lt
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
hi : PPow2 i
ne : i ≠ 2
⊢ 2 < i
Tactic:
by_contra A
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
hi : PPow2 i
ne : i ≠ 2
A : ¬2 < i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_lt
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
hi : PPow2 i
ne : i ≠ 2
A : ¬2 < i
⊢ False
Tactic:
simp [ne, le_iff_lt_or_eq, lt_two_iff_le_one] at A
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
hi : PPow2 i
ne : i ≠ 2
A : i = 0 ∨ i = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_lt
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
hi : PPow2 i
ne : i ≠ 2
A : i = 0 ∨ i = 1
⊢ False
Tactic:
rcases A with (rfl | rfl) <;> simp at hi
Proof state after:
no goals