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

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