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

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => maxLog b x
Tactic:
simp_rw [maxLog]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => (max b.exp x).log

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => (max b.exp x).log
Tactic:
rw [continuous_iff_continuousAt]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun x => (max b.exp x).log) x

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun x => (max b.exp x).log) x
Tactic:
intro x
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => (max b.exp x).log) x

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => (max b.exp x).log) x
Tactic:
refine (ContinuousAt.log ?_ max_exp_pos.ne').comp ?_
State after:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (max b.exp) x

case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => x) x

State before:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (max b.exp) x
Tactic:
apply Continuous.continuousAt
State after:
case refine_1.h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous (max b.exp)

State before:
case refine_1.h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous (max b.exp)
Tactic:
apply Continuous.max
State after:
case refine_1.h.hf
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b_1 => b.exp

case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b

State before:
case refine_1.h.hf
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b_1 => b.exp

case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Tactic:
exact continuous_const
State after:
case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b

State before:
case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Tactic:
exact continuous_id
State after:
no goals

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => x) x
Tactic:
exact continuousAt_id
State after:
no goals