Theorem: LO.FirstOrder.Arith.Model.lt_exp_iff (Arithmetization/ISigmaOne/Bit.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ (∀ j ∈ a, j < i) → a < exp i
Tactic:
contrapose
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ ¬a < exp i → ¬∀ j ∈ a, j < i

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ ¬a < exp i → ¬∀ j ∈ a, j < i
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ exp i ≤ a → ∃ x ∈ a, i ≤ x

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
⊢ exp i ≤ a → ∃ x ∈ a, i ≤ x
Tactic:
intro (h : exp i ≤ a)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
⊢ ∃ x ∈ a, i ≤ x

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
⊢ ∃ x ∈ a, i ≤ x
Tactic:
have pos : 0 < a := lt_of_lt_of_le (by simp) h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
pos : 0 < a
⊢ ∃ x ∈ a, i ≤ x

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
pos : 0 < a
⊢ ∃ x ∈ a, i ≤ x
Tactic:
exact ⟨log a, log_mem_of_pos pos, (exp_le_iff_le_log pos).mp 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 ⊧ₘ* 𝐈𝚺₁
a i : M
h : exp i ≤ a
⊢ 0 < exp i
Tactic:
simp
State after:
no goals