rcases log_pos pos with ⟨_, _, H, _⟩
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
pos : 0 < a
⊢ a < 2 * exp log a
case 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 : M
pos : 0 < a
w✝ : M
left✝ : w✝ ≤ a
H : Exponential (log a) w✝
right✝ : a < 2 * w✝
⊢ a < 2 * exp log a