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

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
h : b.exp ≤ x
⊢ maxLog b x = x.log
Tactic:
simp [maxLog, max_eq_right h]
State after:
no goals