Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff (Arithmetization/OmegaOne/Basic.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 ⊧ₘ omegaOneAxiom ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ ^ 2) y
Tactic:
simp [models_def, omegaOneAxiom, length_defined.df.iff, Exponential.defined.df.iff, sq, ←le_iff_lt_succ]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
constructor
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) → ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y) → ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) → ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
intro h x
State after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x : M
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y

State before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x : M
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
rcases h x with ⟨y, _, _, rfl, h⟩
State after:
case mp.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x y : M
left✝ : ‖x‖ ≤ x
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y

State before:
case mp.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x y : M
left✝ : ‖x‖ ≤ x
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
exact ⟨y, h⟩
State after:
no goals

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y) → ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
intro h x
State after:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x : M
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1

State before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x : M
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
rcases h x with ⟨y, h⟩
State after:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1

State before:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
exact ⟨y, ‖x‖, by simp, rfl, h⟩
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 ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ‖x‖ ≤ x
Tactic:
simp
State after:
no goals