-- Mathlib/Analysis/Complex/AbsMax.lean
/-- If `f` is a function differentiable on the open unit ball, and there exists an `r < 1` such that
any value of `‖f‖` on the open ball is bounded above by some value on the closed ball of radius `r`,
then `f` is constant. -/
lemma eq_const_of_exists_le [ProperSpace E] {f : E → F} {r b : ℝ}
    (h_an : DifferentiableOn ℂ f (ball 0 b)) (hr_nn : 0 ≤ r) (hr_lt : r < b)
    (hr : ∀ z, z ∈ (ball 0 b) → ∃ w, w ∈ closedBall 0 r ∧ ‖f z‖ ≤ ‖f w‖) :
    Set.EqOn f (Function.const E (f 0)) (ball 0 b)

Proof state:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
z : E
hz : z ∈ ball 0 b
w : E
hw : w ∈ closedBall 0 r
hw' : ‖f z‖ ≤ ‖f w‖
⊢ z ∈ {x_1 | (fun x_2 => (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1}

Tactic:
exact hw'.trans (hx_max hw)

Result:
no goals

Proof state:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
obtain ⟨x, hx_mem, hx_max⟩ := isCompact_closedBall (0 : E) r |>.exists_isMaxOn
  (nonempty_closedBall.mpr hr_nn)
  (h_an.continuousOn.mono <| closedBall_subset_ball hr_lt).norm

Result:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Proof state:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
⊢ EqOn f (Function.const E (f x)) (ball 0 b)

Tactic:
apply eq_const_of_exists_max h_an (closedBall_subset_ball hr_lt hx_mem) (fun z hz ↦ ?_)

Result:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
z : E
hz : z ∈ ball 0 b
⊢ z ∈ {x_1 | (fun x_2 => (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1}

Proof state:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
this : EqOn f (Function.const E (f x)) (ball 0 b)
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]

Result:
no goals

Proof state:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
z : E
hz : z ∈ ball 0 b
⊢ z ∈ {x_1 | (fun x_2 => (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1}

Tactic:
obtain ⟨w, hw, hw'⟩ := hr z hz

Result:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
z : E
hz : z ∈ ball 0 b
w : E
hw : w ∈ closedBall 0 r
hw' : ‖f z‖ ≤ ‖f w‖
⊢ z ∈ {x_1 | (fun x_2 => (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1}

Proof state:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
⊢ EqOn f (Function.const E (f 0)) (ball 0 b)

Tactic:
suffices Set.EqOn f (Function.const E (f x)) (ball 0 b) by
  rwa [this (mem_ball_self (hr_nn.trans_lt hr_lt))]

Result:
case intro.intro
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x => ‖f x‖) (closedBall 0 r) x
⊢ EqOn f (Function.const E (f x)) (ball 0 b)