internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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
ne : i ≠ 2
⊢ 4 ≤ 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 : ¬4 ≤ i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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
ne : i ≠ 2
A : ¬4 ≤ i
⊢ False
Tactic:
have : i ≤ 3 := by simpa [←three_add_one_eq_four, ←le_iff_lt_succ] 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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne : i ≠ 2
A : ¬4 ≤ i
this : i ≤ 3
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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
ne : i ≠ 2
A : ¬4 ≤ i
this : i ≤ 3
⊢ False
Tactic:
rcases le_three_iff_eq_zero_or_one_or_two_or_three.mp this with (rfl | rfl | rfl | rfl) <;> simp at ne hi
Proof state after:
case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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
ne : i ≠ 2
A : ¬4 ≤ i
⊢ i ≤ 3
Tactic:
simpa [←three_add_one_eq_four, ←le_iff_lt_succ] using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_le
Proof state before:
case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ False
Tactic:
have : PPow2 (1 : M) := by simpa [sqrt_three] using hi.sqrt (by simp)
Proof state after:
case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this✝ : 3 ≤ 3
ne : True
this : PPow2 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_le
Proof state before:
case inr.inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this✝ : 3 ≤ 3
ne : True
this : PPow2 1
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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 ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ PPow2 1
Tactic:
simpa [sqrt_three] using hi.sqrt (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.four_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 ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ 3 ≠ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
⊢ i ^ 2 ≠ 2
Tactic:
intro e
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
e : i ^ 2 = 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
e : i ^ 2 = 2
⊢ False
Tactic:
have : i < 2 := by simpa [←e] using lt_square_of_lt hi.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
hi : PPow2 i
e : i ^ 2 = 2
this : i < 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
e : i ^ 2 = 2
this : i < 2
⊢ False
Tactic:
exact not_le.mpr this hi.two_le
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
e : i ^ 2 = 2
⊢ i < 2
Tactic:
simpa [←e] using lt_square_of_lt hi.one_lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne2 : i ≠ 2
ne4 : i ≠ 4
⊢ √i ≠ 2
Tactic:
intro e
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
ne2 : i ≠ 2
ne4 : i ≠ 4
e : √i = 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne2 : i ≠ 2
ne4 : i ≠ 4
e : √i = 2
⊢ False
Tactic:
have : i = 4 := by simpa [e, two_pow_two_eq_four] using Eq.symm <| hi.sq_sqrt_eq ne2
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
ne2 : i ≠ 2
ne4 : i ≠ 4
e : √i = 2
this : i = 4
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne2 : i ≠ 2
ne4 : i ≠ 4
e : √i = 2
this : i = 4
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sqrt_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne2 : i ≠ 2
ne4 : i ≠ 4
e : √i = 2
⊢ i = 4
Tactic:
simpa [e, two_pow_two_eq_four] using Eq.symm <| hi.sq_sqrt_eq ne2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_ne_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : PPow2 i
ne2 : i ≠ 2
⊢ i ^ 2 ≠ 4
Tactic:
simpa [two_pow_two_eq_four] using ne_of_gt (sq_lt_sq.mpr (hi.two_lt ne2))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
⊢ 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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
⊢ i ^ 2 ≤ j
Tactic:
suffices ∀ i < j, PPow2 i → PPow2 j → i^2 ≤ j from this i hij 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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
⊢ ∀ i < j, PPow2 i → PPow2 j → i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
hij : i < j
⊢ ∀ i < j, PPow2 i → PPow2 j → i ^ 2 ≤ j
Tactic:
clear hi hij 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 ⊧ₘ* 𝐈𝚫₀
i j : M
⊢ ∀ i < j, PPow2 i → PPow2 j → i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
⊢ ∀ i < j, PPow2 i → PPow2 j → 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 ⊧ₘ* 𝐈𝚫₀
i : M
⊢ 𝚺₀-Predicate fun {j} => ∀ i < j, PPow2 i → PPow2 j → 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 ⊧ₘ* 𝐈𝚫₀
i x✝ : M
a✝ : ∀ y < x✝, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
⊢ ∀ i < x✝, PPow2 i → PPow2 x✝ → i ^ 2 ≤ x✝
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i : M
⊢ 𝚺₀-Predicate fun {j} => ∀ i < j, PPow2 i → PPow2 j → i ^ 2 ≤ j
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
⊢ ∀ i < j, PPow2 i → PPow2 j → i ^ 2 ≤ j
Tactic:
intro i hij 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
⊢ i ^ 2 ≤ j
Tactic:
by_cases ej : 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : j = 2
⊢ i ^ 2 ≤ j
Tactic:
have : 2 ≤ i := by simpa [one_add_one_eq_two] using lt_iff_succ_le.mp hi.one_lt
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✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : j = 2
this : 2 ≤ i
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : j = 2
this : 2 ≤ i
⊢ i ^ 2 ≤ j
Tactic:
exact False.elim ((not_lt.mpr this) (by simpa [ej] using hij))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : j = 2
⊢ 2 ≤ i
Tactic:
simpa [one_add_one_eq_two] using lt_iff_succ_le.mp hi.one_lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : j = 2
this : 2 ≤ i
⊢ i < 2
Tactic:
simpa [ej] using hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
⊢ i ^ 2 ≤ j
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✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : i = 2
⊢ i ^ 2 ≤ j
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 ⊧ₘ* 𝐈𝚫₀
i j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
hj : PPow2 j
ej : ¬j = 2
hij : 2 < j
hi : PPow2 2
⊢ 2 ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
hj : PPow2 j
ej : ¬j = 2
hij : 2 < j
hi : PPow2 2
⊢ 2 ^ 2 ≤ j
Tactic:
simpa [sq, two_mul_two_eq_four] using hj.four_le ej
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
⊢ i ^ 2 ≤ j
Tactic:
have : √i < √j := by
  by_contra A
  have : j ≤ i := by simpa [hi.sq_sqrt_eq ei, hj.sq_sqrt_eq ej] 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
this : √i < √j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
this : √i < √j
⊢ i ^ 2 ≤ j
Tactic:
have : i ≤ √j := by
  simpa [hi.sq_sqrt_eq ei] using
    IH (√j) (sqrt_lt_self_of_one_lt hj.one_lt) (√i) this (hi.sqrt ei) (hj.sqrt ej)
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✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
this✝ : √i < √j
this : i ≤ √j
⊢ i ^ 2 ≤ j
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
this✝ : √i < √j
this : i ≤ √j
⊢ i ^ 2 ≤ j
Tactic:
simpa [hj.sq_sqrt_eq ej] using sq_le_sq.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
⊢ False
Tactic:
have : j ≤ i := by simpa [hi.sq_sqrt_eq ei, hj.sq_sqrt_eq ej] 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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
this : j ≤ i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬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.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
⊢ j ≤ i
Tactic:
simpa [hi.sq_sqrt_eq ei, hj.sq_sqrt_eq ej] using sq_le_sq.mpr (show √j ≤ √i from by simpa using A)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
⊢ √j ≤ √i
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
A : ¬√i < √j
this : j ≤ i
⊢ i < j
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.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 ⊧ₘ* 𝐈𝚫₀
i✝ j : M
IH : ∀ y < j, ∀ i < y, PPow2 i → PPow2 y → i ^ 2 ≤ y
i : M
hij : i < j
hi : PPow2 i
hj : PPow2 j
ej : ¬j = 2
ei : ¬i = 2
this : √i < √j
⊢ i ≤ √j
Tactic:
simpa [hi.sq_sqrt_eq ei] using
  IH (√j) (sqrt_lt_self_of_one_lt hj.one_lt) (√i) this (hi.sqrt ei) (hj.sqrt ej)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
⊢ i = j
Tactic:
by_contra ne
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
⊢ False
Tactic:
wlog hij : i < j
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
⊢ False
Tactic:
have : y^2 < y^2 := calc
  y^2 < i^2 := sq_lt_sq.mpr hi.1
  _   ≤ j   := sq_le_of_lt ppi ppj hij
  _   ≤ y^2 := hj.2
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
this : y ^ 2 < y ^ 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
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 : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
hij : i < j
this : y ^ 2 < y ^ 2
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
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 ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False
Tactic:
exact this py ppj ppi hj hi (Ne.symm ne) (Ne.lt_of_le' ne (by simpa using hij))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ y ^ 2
hj : y < j ∧ j ≤ y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ y ^ 2 → y < j ∧ j ≤ y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ j ≤ i
Tactic:
simpa using hij
Proof state after:
no goals