-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem norm_circleTransformBoundingFunction_le {R r : ℝ} (hr : r < R) (hr' : 0 ≤ r) (z : ℂ) :
    ∃ x : closedBall z r ×ˢ [[0, 2 * π]], ∀ y : closedBall z r ×ˢ [[0, 2 * π]],
    ‖circleTransformBoundingFunction R z y‖ ≤ ‖circleTransformBoundingFunction R z x‖

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
simpa [isMaxOn_iff] using this

Result:
no goals

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty :=
  (nonempty_closedBall.2 hr').prod nonempty_uIcc

Result:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ IsCompact (closedBall z r ×ˢ [[0, 2 * π]])

Tactic:
apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]

Result:
no goals

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have := IsCompact.exists_isMaxOn comp none (cts.mono <| prod_mono_right (subset_univ _))

Result:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have cts := continuousOn_norm_circleTransformBoundingFunction hr z

Result:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Proof state:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
  apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]

Result:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x => ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖