y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x
y : ℝ
⊢ Continuous fun a => a ^ y
refine continuous_iff_continuousAt.2 fun x => ?_
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x

case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x

case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x
rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
no goals
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x
exact continuousAt_rpow_const_of_pos hy
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x
simp only [rpow_zero]
no goals
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x
exact continuousAt_const
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x
obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x
have z_pos : 0 < z := by simpa [hz] using hy
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x
simp_rw [hz, rpow_neg]
no goals
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x
exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)
no goals
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z
simpa [hz] using hy