internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.SPPow2.one_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
hi : LenBit i m
A : ¬1 < i
⊢ False
Tactic:
rcases (le_one_iff_eq_zero_or_one.mp (show i ≤ 1 from by simpa using A)) with (rfl | rfl)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
hi : LenBit 0 m
A : ¬1 < 0
⊢ False

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
hi : LenBit 1 m
A : ¬1 < 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.one_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
hi : LenBit i m
A : ¬1 < i
⊢ i ≤ 1
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.one_lt
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
hi : LenBit 0 m
A : ¬1 < 0
⊢ False
Tactic:
simp at hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.one_lt
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
hi : LenBit 1 m
A : ¬1 < 1
⊢ False
Tactic:
exact hm.1 hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
⊢ LenBit i m
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : i = 1
⊢ LenBit i m

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
⊢ LenBit i m
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : i = 1
⊢ LenBit i m
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
hm : SPPow2 m
pi : Pow2 1
him : 1 ≤ m
hsqi : (√1) ^ 2 = 1
hi : LenBit (√1) m
⊢ LenBit 1 m
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt
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
hm : SPPow2 m
pi : Pow2 1
him : 1 ≤ m
hsqi : (√1) ^ 2 = 1
hi : LenBit (√1) m
⊢ LenBit 1 m
Tactic:
simpa using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
⊢ LenBit i m
Tactic:
have ne2 : i ≠ 2 := by
  rintro rfl; simp [sqrt_two] at hsqi
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
ne2 : i ≠ 2
⊢ LenBit i m
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
ne2 : i ≠ 2
⊢ LenBit i m
Tactic:
have : 2 < i := lt_of_le_of_ne
  (one_lt_iff_two_le.mp <| lt_of_le_of_ne (pos_iff_one_le.mp pi.pos) <| Ne.symm ne1) (Ne.symm ne2)
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
ne2 : i ≠ 2
this : 2 < i
⊢ LenBit i m
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
ne2 : i ≠ 2
this : 2 < i
⊢ LenBit i m
Tactic:
exact (hm.lenbit_iff him pi this).mpr ⟨hsqi, hi⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
⊢ i ≠ 2
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
hm : SPPow2 m
pi : Pow2 2
him : 2 ≤ m
hsqi : (√2) ^ 2 = 2
hi : LenBit (√2) m
ne1 : ¬2 = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
pi : Pow2 2
him : 2 ≤ m
hsqi : (√2) ^ 2 = 2
hi : LenBit (√2) m
ne1 : ¬2 = 1
⊢ False
Tactic:
simp [sqrt_two] at hsqi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ ¬LenBit 1 2
Tactic:
simp[LenBit.one]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ LenBit 2 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ ∀ i ≤ 2, Pow2 i → 2 < i → (LenBit i 2 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 2)
Tactic:
intro i hi pi
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
hm : SPPow2 m
i : M
hi : i ≤ 2
pi : Pow2 i
⊢ 2 < i → (LenBit i 2 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 2)
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
hi : i ≤ 2
pi : Pow2 i
⊢ 2 < i → (LenBit i 2 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 2)
Tactic:
rcases le_two_iff_eq_zero_or_one_or_two.mp hi with (rfl | rfl | rfl) <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ ¬SPPow2 0
Tactic:
rintro ⟨_, h, _⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
left✝ : ¬LenBit 1 0
h : LenBit 2 0
right✝ : ∀ i ≤ 0, Pow2 i → 2 < i → (LenBit i 0 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 0)
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.not_zero
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
left✝ : ¬LenBit 1 0
h : LenBit 2 0
right✝ : ∀ i ≤ 0, Pow2 i → 2 < i → (LenBit i 0 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 0)
⊢ False
Tactic:
simp at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ ¬SPPow2 1
Tactic:
rintro ⟨_, h, _⟩
Proof state after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
left✝ : ¬LenBit 1 1
h : LenBit 2 1
right✝ : ∀ i ≤ 1, Pow2 i → 2 < i → (LenBit i 1 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 1)
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.not_one
Proof state before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
left✝ : ¬LenBit 1 1
h : LenBit 2 1
right✝ : ∀ i ≤ 1, Pow2 i → 2 < i → (LenBit i 1 ↔ (√i) ^ 2 = i ∧ LenBit (√i) 1)
⊢ False
Tactic:
simp [LenBit.iff_rem, one_lt_two] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
⊢ i < j → i ^ 2 ≤ j
Tactic:
intro hij
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
hm : SPPow2 m
i j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
hij : i < j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
hij : i < j
⊢ i ^ 2 ≤ j
Tactic:
suffices ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i^2 ≤ j from this i hij pi pj hi hj
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
hm : SPPow2 m
i j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
hij : i < j
⊢ ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
hij : i < j
⊢ ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Tactic:
clear i pi hi hij pj hj
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
hm : SPPow2 m
j : M
⊢ ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
⊢ ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Tactic:
induction j using order_induction_iSigmaZero
Proof state after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ 𝚺₀-Predicate fun {j} => ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
x✝ : M
a✝ : ∀ y < x✝, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
⊢ ∀ i < x✝, Pow2 i → Pow2 x✝ → LenBit i m → LenBit x✝ m → i ^ 2 ≤ x✝
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
Proof state before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
⊢ 𝚺₀-Predicate fun {j} => ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
⊢ ∀ i < j, Pow2 i → Pow2 j → LenBit i m → LenBit j m → i ^ 2 ≤ j
Tactic:
intro i hij pi pj  hi hj
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
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
⊢ i ^ 2 ≤ j
Tactic:
by_cases jne2 : j = 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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : j = 2
⊢ i ^ 2 ≤ j

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : j = 2
⊢ i ^ 2 ≤ j
Tactic:
rcases jne2 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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
hi : LenBit i m
IH : ∀ y < 2, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
hij : i < 2
pj : Pow2 2
hj : LenBit 2 m
⊢ i ^ 2 ≤ 2
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
hi : LenBit i m
IH : ∀ y < 2, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
hij : i < 2
pj : Pow2 2
hj : LenBit 2 m
⊢ i ^ 2 ≤ 2
Tactic:
have : 2 ≤ i := one_lt_iff_two_le.mp (hm.one_lt hi)
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
hi : LenBit i m
IH : ∀ y < 2, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
hij : i < 2
pj : Pow2 2
hj : LenBit 2 m
this : 2 ≤ i
⊢ i ^ 2 ≤ 2
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
hi : LenBit i m
IH : ∀ y < 2, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
hij : i < 2
pj : Pow2 2
hj : LenBit 2 m
this : 2 ≤ i
⊢ i ^ 2 ≤ 2
Tactic:
exact False.elim ((not_lt.mpr this) hij)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
⊢ i ^ 2 ≤ j
Tactic:
by_cases ine2 : 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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : i = 2
⊢ i ^ 2 ≤ j

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : i = 2
⊢ i ^ 2 ≤ j
Tactic:
rcases ine2 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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
pj : Pow2 j
hj : LenBit j m
jne2 : ¬j = 2
hij : 2 < j
pi : Pow2 2
hi : LenBit 2 m
⊢ 2 ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
pj : Pow2 j
hj : LenBit j m
jne2 : ¬j = 2
hij : 2 < j
pi : Pow2 2
hi : LenBit 2 m
⊢ 2 ^ 2 ≤ j
Tactic:
simpa [sq, two_mul_two_eq_four] using pj.four_le hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
⊢ i ^ 2 ≤ j
Tactic:
have : √i < √j := by
  by_contra A
  have : j ≤ i := by
    simpa [hm.sq_sqrt_eq hi pi ine2, hm.sq_sqrt_eq hj pj jne2] using
      sq_le_sq.mpr (show √j ≤ √i from by simpa using A)
  exact False.elim ((not_lt.mpr this) (by simpa using hij))
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
this : √i < √j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
this : √i < √j
⊢ i ^ 2 ≤ j
Tactic:
have : i ≤ √j := by
  simpa [hm.sq_sqrt_eq hi pi ine2] using
    IH (√j) (sqrt_lt_self_of_one_lt (hm.one_lt hj)) (√i) this
      (pi.sqrt (hm.sq_sqrt_eq hi pi ine2)) (pj.sqrt (hm.sq_sqrt_eq hj pj jne2)) (hm.sqrt hi pi ine2) (hm.sqrt hj pj jne2)
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
this✝ : √i < √j
this : i ≤ √j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_lt
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
this✝ : √i < √j
this : i ≤ √j
⊢ i ^ 2 ≤ j
Tactic:
simpa [hm.sq_sqrt_eq hj pj jne2] using sq_le_sq.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
⊢ √i < √j
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
⊢ False
Tactic:
have : j ≤ i := by
  simpa [hm.sq_sqrt_eq hi pi ine2, hm.sq_sqrt_eq hj pj jne2] using
    sq_le_sq.mpr (show √j ≤ √i from by simpa using 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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
this : j ≤ i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
this : j ≤ i
⊢ False
Tactic:
exact False.elim ((not_lt.mpr this) (by simpa using hij))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
⊢ j ≤ i
Tactic:
simpa [hm.sq_sqrt_eq hi pi ine2, hm.sq_sqrt_eq hj pj jne2] using
  sq_le_sq.mpr (show √j ≤ √i from by simpa using A)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
⊢ √j ≤ √i
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.sq_le_of_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
j : M
IH : ∀ y < j, ∀ i < y, Pow2 i → Pow2 y → LenBit i m → LenBit y m → i ^ 2 ≤ y
i : M
hij : i < j
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
jne2 : ¬j = 2
ine2 : ¬i = 2
A : ¬√i < √j
this : j ≤ i
⊢ i < j
Tactic:
simpa using hij
Proof state after:
no goals