Theorem: LO.FirstOrder.Arith.Model.Exponential.exponential_one_two (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≤ 2 ^ 4
Tactic:
simp [pow_four_eq_sq_sq, two_pow_two_eq_four]
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 ⊧ₘ* 𝐈𝚫₀
⊢ 2 * 4 ≤ 2 ^ 4
Tactic:
simp [pow_four_eq_sq_sq, two_pow_two_eq_four, sq (4 : M)]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 ≤ 4

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 2 ≤ 4
Tactic:
exact le_of_lt two_lt_four
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 ⊧ₘ* 𝐈𝚫₀
⊢ Seq₀ 4 (2 * 4)
Tactic:
simp [Seq₀, ext, one_lt_four, two_lt_four]
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 ⊧ₘ* 𝐈𝚫₀
⊢ Seqₛ 2 4 (2 * 4)
Tactic:
simp [Seqₛ]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∀ u ≤ 2, ¬u = 2 → PPow2 u → Seqₛ.Even 4 (2 * 4) u ∨ Seqₛ.Odd 4 (2 * 4) u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ∀ u ≤ 2, ¬u = 2 → PPow2 u → Seqₛ.Even 4 (2 * 4) u ∨ Seqₛ.Odd 4 (2 * 4) u
Tactic:
intro i hi ne2 ppi
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 : i ≤ 2
ne2 : ¬i = 2
ppi : PPow2 i
⊢ Seqₛ.Even 4 (2 * 4) i ∨ Seqₛ.Odd 4 (2 * 4) i

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 : i ≤ 2
ne2 : ¬i = 2
ppi : PPow2 i
⊢ Seqₛ.Even 4 (2 * 4) i ∨ Seqₛ.Odd 4 (2 * 4) i
Tactic:
exact False.elim <| not_le.mpr (ppi.two_lt ne2) 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 ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≤ 2 ^ 2
Tactic:
simp [two_pow_two_eq_four]
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 ⊧ₘ* 𝐈𝚫₀
⊢ 4 ≠ 2
Tactic:
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 ⊧ₘ* 𝐈𝚫₀
⊢ PPow2 4 ∧ ext 4 4 = 1 ∧ ext 4 (2 * 4) = 2
Tactic:
simp [ext, one_lt_four, two_lt_four]
State after:
no goals