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

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

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ max b.exp x ≤ y.exp
Tactic:
apply max_le
State after:
case h₁
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ b.exp ≤ y.exp

case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp

State before:
case h₁
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ b.exp ≤ y.exp

case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Tactic:
apply Real.exp_le_exp.mpr yb
State after:
case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp

State before:
case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Tactic:
exact xy
State after:
no goals