Theorem: LO.FirstOrder.Arith.Model.SPPow2.of_sqrt (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 : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
⊢ LenBit i m
Tactic:
by_cases ne1 : i = 1
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

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

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

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

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⟩
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
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
⊢ i ≠ 2
Tactic:
rintro rfl
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

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