-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_eqOn_closedBall_of_isMaxOn {f : E → F} {z : E} {r : ℝ}
    (hd : DiffContOnCl ℂ f (ball z r)) (hz : IsMaxOn (norm ∘ f) (ball z r) z) :
    EqOn (norm ∘ f) (const E ‖f z‖) (closedBall z r)

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

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

Result:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

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

Result:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Tactic:
have hr : dist (1 : ℂ) 0 = 1 := by simp

Result:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
this : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
simpa [e]

Result:
no goals

Proof state:
case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z

Tactic:
rfl

Result:
no goals

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa [e]

Result:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
rcases eq_or_ne z w with (rfl | hne)

Result:
case inl
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hw : dist z z ≤ r
⊢ (norm ∘ f) z = Function.const E ‖f z‖ z

case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
hball : MapsTo e (ball 0 1) (ball z r)
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Tactic:
exact norm_max_aux₃ hr (hd.comp hde.diffContOnCl hball)
    (hz.comp_mapsTo hball (lineMap_apply_zero z w))

Result:
no goals

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
rw [mem_closedBall, dist_comm] at hw

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Proof state:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖

Tactic:
have hball : MapsTo e (ball 0 1) (ball z r) := by
  refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
    Subset.rfl ?_
  simpa only [lineMap_apply_zero, mul_one, coe_nndist] using ball_subset_ball hw

Result:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
hball : MapsTo e (ball 0 1) (ball z r)
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖