Theorem: le_exp_maxLog (Ray/Hartogs/MaxLog.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ (maxLog b x).exp
Tactic:
rw [maxLog, Real.exp_log max_exp_pos]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ max b.exp x

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ max b.exp x
Tactic:
bound
State after:
no goals