-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : IsBounded U)
    (hd : DiffContOnCl ℂ f U) {C : ℝ} (hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C) {z : E}
    (hz : z ∈ closure U) : ‖f z‖ ≤ C

Proof state:
case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C

Tactic:
rcases exists_ne z with ⟨w, hne⟩

Result:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C

Proof state:
case inr.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C

Tactic:
calc
  ‖f z‖ = ‖f (e 0)‖ := by simp only [e, lineMap_apply_zero]
  _ ≤ ‖f (e ζ)‖ := hζ (subset_closure h₀)
  _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)

Result:
no goals

Proof state:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C

Tactic:
have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm

Result:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ = ‖f (e 0)‖

Tactic:
simp only [e, lineMap_apply_zero]

Result:
no goals

Proof state:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
⊢ ‖f z‖ ≤ C

Tactic:
rcases exists_mem_frontier_isMaxOn_norm (hL.isBounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩

Result:
case inr.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C

Proof state:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C

Tactic:
set e := (lineMap z w : ℂ → E)

Result:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
⊢ ‖f z‖ ≤ C

Proof state:
case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

Tactic:
exact hC z hz

Result:
no goals

Proof state:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C

Tactic:
replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U) :=
  hd.comp hde.diffContOnCl (mapsTo_preimage _ _)

Result:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C

Proof state:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
⊢ ‖f z‖ ≤ C

Tactic:
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z

Result:
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C