[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : C(α, β)
⊢ (mkOfCompact f).toContinuousMap = f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : C(α, β)
a✝ : α
⊢ ↑(mkOfCompact f).toContinuousMap a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : α →ᵇ β
⊢ mkOfCompact f.toContinuousMap = f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f : α →ᵇ β
x✝ : α
⊢ ↑(mkOfCompact f.toContinuousMap) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t,
        t ∈ uniformity (α →ᵇ β) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
[PROOFSTEP]
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.fst ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.fst p.snd ≤ i_1} ⊆ i.snd) ∧
          {fg | ∀ (x : α), x ∈ i.fst → (↑fg.fst x, ↑fg.snd x) ∈ i.snd} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.fst p.snd ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
[PROOFSTEP]
exact fun s =>
  ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
    ⟨{p | ∀ x, (p.1 x, p.2 x) ∈ b}, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩, fun f g h => hs fun x _ => h x⟩,
    fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
    ⟨⟨Set.univ, {p | dist p.1 p.2 ≤ ε}⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩, fun ⟨f, g⟩ h =>
      hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
x : α
⊢ dist (↑f x) (↑g x) ≤ dist f g
[PROOFSTEP]
simp only [← dist_mkOfCompact, dist_coe_le_dist, ← mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le C0, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : MetricSpace β
inst✝¹ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (↑f x) (↑g x) ≤ C
[PROOFSTEP]
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le_iff_of_nonempty, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : MetricSpace β
inst✝¹ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist (↑(mkOfCompact f) x) (↑(mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (↑f x) (↑g x) < C
[PROOFSTEP]
simp only [mkOfCompact_apply]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
src✝¹ : MetricSpace C(α, E) := metricSpace α E
src✝ : AddCommGroup C(α, E) := instAddCommGroupContinuousMap
x y : C(α, E)
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm, mkOfCompact_sub]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : MetricSpace β
inst✝³ : NormedAddCommGroup E
inst✝² : Nonempty α
inst✝¹ : One E
inst✝ : NormOneClass E
⊢ ‖1‖ = 1
[PROOFSTEP]
simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]
[GOAL]
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
inst✝³ : MetricSpace β
inst✝² : NormedAddCommGroup E
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
src✝ : C(α, E) ≃+ (α →ᵇ E) := addEquivBoundedOfCompact α E
c : 𝕜
f : C(α, E)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : C(α, E)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (c • f) =
    ↑(RingHom.id 𝕜) c •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : C(α, E)),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
inst✝³ : MetricSpace β
inst✝² : NormedAddCommGroup E
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
src✝ : C(α, E) ≃+ (α →ᵇ E) := addEquivBoundedOfCompact α E
c : 𝕜
f : C(α, E)
x✝ : α
⊢ ↑(AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : C(α, E)),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
          (c • f))
      x✝ =
    ↑(↑(RingHom.id 𝕜) c •
          AddHom.toFun
            { toFun := src✝.toFun,
              map_add' :=
                (_ :
                  ∀ (x y : C(α, E)),
                    Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
            f)
      x✝
[PROOFSTEP]
norm_cast
[GOAL]
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
⊢ ↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g
[PROOFSTEP]
ext f
[GOAL]
case h.h
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : NormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ ↑(↑↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ =
    ↑(↑(ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
⊢ Continuous fun g => comp g f
[PROOFSTEP]
refine' Metric.continuous_iff.mpr _
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
⊢ ∀ (b : C(Y, T)) (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : C(Y, T)), dist a b < δ → dist (comp a f) (comp b f) < ε
[PROOFSTEP]
intro g ε ε_pos
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (a : C(Y, T)), dist a g < δ → dist (comp a f) (comp g f) < ε
[PROOFSTEP]
refine' ⟨ε, ε_pos, fun g' h => _⟩
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
g' : C(Y, T)
h : dist g' g < ε
⊢ dist (comp g' f) (comp g f) < ε
[PROOFSTEP]
rw [ContinuousMap.dist_lt_iff ε_pos] at h ⊢
[GOAL]
X : Type u_1
Y : Type u_2
T : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace Y
inst✝ : MetricSpace T
f : C(X, Y)
g : C(Y, T)
ε : ℝ
ε_pos : ε > 0
g' : C(Y, T)
h : ∀ (x : Y), dist (↑g' x) (↑g x) < ε
⊢ ∀ (x : X), dist (↑(comp g' f) x) (↑(comp g f) x) < ε
[PROOFSTEP]
exact fun x => h (f x)
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
⊢ Summable F
[PROOFSTEP]
refine' (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => _
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Tendsto (fun i => restrict K (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
lift K to Compacts X using hK
[GOAL]
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
have A : ∀ s : Finset ι, restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict K (F i) :=
  by
  intro s
  ext1 x
  simp
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
[PROOFSTEP]
intro s
[GOAL]
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
[PROOFSTEP]
ext1 x
[GOAL]
case h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ↑(restrict (↑K) (∑ i in s, F i)) x = ↑(∑ i in s, restrict (↑K) (F i)) x
[PROOFSTEP]
simp
[GOAL]
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
[PROOFSTEP]
simpa only [HasSum, A] using summable_of_summable_norm (hF K)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : StarAddMonoid β
inst✝¹ : NormedStarGroup β
inst✝ : CompactSpace α
f : C(α, β)
⊢ ‖star f‖ = ‖f‖
[PROOFSTEP]
rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star, norm_star,
  BoundedContinuousFunction.norm_mkOfCompact]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖star f * f‖ = ‖f‖ * ‖f‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖star f * f‖ ≤ ‖f‖ * ‖f‖
[PROOFSTEP]
rw [← sq, ContinuousMap.norm_le _ (sq_nonneg _)]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖↑(star f * f) x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
intro x
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑(star f * f) x‖ ≤ ‖f‖ ^ 2
[PROOFSTEP]
simp only [ContinuousMap.coe_mul, coe_star, Pi.mul_apply, Pi.star_apply, CstarRing.norm_star_mul_self, ← sq]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ^ 2 ≤ ‖f‖ ^ 2
[PROOFSTEP]
refine' sq_le_sq' _ _
[GOAL]
case refine'_1.refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ -‖f‖ ≤ ‖↑f x‖
[PROOFSTEP]
linarith [norm_nonneg (f x), norm_nonneg f]
[GOAL]
case refine'_1.refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ≤ ‖f‖
[PROOFSTEP]
exact ContinuousMap.norm_coe_le_norm f x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
[PROOFSTEP]
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖↑f x‖ ≤ Real.sqrt ‖star f * f‖
[PROOFSTEP]
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CstarRing.norm_star_mul_self]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedRing β
inst✝² : StarRing β
inst✝¹ : CompactSpace α
inst✝ : CstarRing β
f : C(α, β)
x : α
⊢ ‖star (↑f x) * ↑f x‖ ≤ ‖star f * f‖
[PROOFSTEP]
exact ContinuousMap.norm_coe_le_norm (star f * f) x
