case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y

case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)
convert ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
no goals
case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y
simp [hy]
no goals
case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤
exact Or.inr hc