-- Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
lemma exist_norm_eq [c : Nonempty α] {f : α →ᵇ γ} (h : f ∈ C_cb(α, γ)) : ∃ (x : α),
    ‖f x‖ = ‖f‖

Proof state:
case pos.intro.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
by_cases hy : y ∈ tsupport f

Result:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∈ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
this : f = 0
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
simp [this]

Result:
no goals

Proof state:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
suffices f = 0 by simp [this]

Result:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ f = 0

Proof state:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∈ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
exact hmax hy

Result:
no goals

Proof state:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ f = 0

Tactic:
rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs

Result:
no goals

Proof state:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
obtain ⟨x, _, hmax⟩ := mem_compactlySupported.mp h |>.exists_isMaxOn hs <|
  (map_continuous f).norm.continuousOn

Result:
case pos.intro.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
⊢ ∃ x, ‖f x‖ = ‖f‖

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
by_cases hs : (tsupport f).Nonempty

Result:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Proof state:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
simp [image_eq_zero_of_nmem_tsupport hy]

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
refine ⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩

Result:
case pos.intro.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x => ‖f x‖) (tsupport ⇑f) x
y : α
⊢ ‖f y‖ ≤ ‖f x‖