Theorem: LO.FirstOrder.Arith.Model.PPow2.sq_le_of_lt (Arithmetization/ISigmaZero/Exponential/PPow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
hi : PPow2 i
hj : PPow2 j
⊢ i < j → i ^ 2 ≤ j
Tactic:
intro hij
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

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
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

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
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

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
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✝

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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i 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
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

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
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

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
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

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))
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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
State after:
no goals

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
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

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
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

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
State after:
no goals

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))
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

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)
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

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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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
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

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)
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

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))
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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)
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i✝ 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)
State after:
no goals