rewrite [← hnormCx, ← hCx]
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < sInf (norm '' (C '' s))
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < (fun a => ‖a‖) (C x)