Theorem: LO.FirstOrder.Arith.Model.lt_exponential_log_self (Arithmetization/ISigmaZero/Exponential/Log.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 b : M
h : Exponential (log a) b
⊢ a < 2 * b
Tactic:
rcases zero_le a with (rfl | pos)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential (log 0) b
⊢ 0 < 2 * b

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
⊢ a < 2 * b

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
⊢ a < 2 * b
Tactic:
rcases log_pos pos with ⟨_, _, H, _⟩
State after:
case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * b

State before:
case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * b
Tactic:
rcases H.uniq h
State after:
case inr.intro.intro.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ a < 2 * b

State before:
case inr.intro.intro.intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
h : Exponential (log a) b
pos : 0 < a
left✝ : b ≤ a
H : Exponential (log a) b
right✝ : a < 2 * b
⊢ a < 2 * b
Tactic:
assumption
State after:
no goals

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : Exponential (log 0) b
⊢ 0 < 2 * b
Tactic:
simp at h
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < 2 * b

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
h : b = 1
⊢ 0 < 2 * b
Tactic:
simp [h]
State after:
no goals