Theorem: LO.FirstOrder.Arith.Model.SPPow2.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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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

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

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)
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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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))
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

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

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
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 ⊧ₘ* 𝐈𝚫₀
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
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

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

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))
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 ⊧ₘ* 𝐈𝚫₀
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)
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 ⊧ₘ* 𝐈𝚫₀
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
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 ⊧ₘ* 𝐈𝚫₀
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
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 ⊧ₘ* 𝐈𝚫₀
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 ≤ √j
Tactic:
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)
State after:
no goals