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

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

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