Theorem: LO.FirstOrder.Arith.Model.PPow2.four_le (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 : M
hi : PPow2 i
ne : i ≠ 2
⊢ 4 ≤ i
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 : M
hi : PPow2 i
ne : i ≠ 2
A : ¬4 ≤ 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 : 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
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

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

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

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

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
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 ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ PPow2 1
Tactic:
simpa [sqrt_three] using hi.sqrt (by simp)
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 ⊧ₘ* 𝐈𝚫₀
hi : PPow2 3
A : ¬4 ≤ 3
this : 3 ≤ 3
ne : True
⊢ 3 ≠ 2
Tactic:
simp
State after:
no goals