awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ circleTransformDeriv R z w f = fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
have h : ∀ (x : ℝ), circleTransformDeriv R z w f x = (circleMap z R x - w)⁻¹ • circleTransform R z w f x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
⊢ circleTransformDeriv R z w f x = (circleMap z R x - w)⁻¹ • circleTransform R z w f x
have h : ((2 * (↑π : ℂ) * I)⁻¹ * deriv (circleMap z R) x * (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹) •
    f (circleMap z R x) =
  ((circleMap z R x - w)⁻¹ * (2 * (↑π : ℂ) * I)⁻¹ * deriv (circleMap z R) x * (circleMap z R x - w)⁻¹) •
    f (circleMap z R x)
Tactic: simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
⊢ ((2 * (↑π : ℂ) * I)⁻¹ * deriv (circleMap z R) x * (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹) •
      f (circleMap z R x) =
    ((circleMap z R x - w)⁻¹ * (2 * (↑π : ℂ) * I)⁻¹ * deriv (circleMap z R) x * (circleMap z R x - w)⁻¹) •
      f (circleMap z R x)
have h : ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x *
        (-(circleMap z R x * w * 2) + HPow.hPow (β := ℕ) (circleMap z R x) 2 + HPow.hPow (β := ℕ) w 2)⁻¹ *
      (1 / 2)) •
    f (circleMap z R x) =
  ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x * HPow.hPow (β := ℕ) (circleMap z R x - w)⁻¹ 2 * (1 / 2)) •
    f (circleMap z R x)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
⊢ ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x *
          (-(circleMap z R x * w * 2) + HPow.hPow (β := ℕ) (circleMap z R x) 2 + HPow.hPow (β := ℕ) w 2)⁻¹ *
        (1 / 2)) •
      f (circleMap z R x) =
    ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x * HPow.hPow (β := ℕ) (circleMap z R x - w)⁻¹ 2 * (1 / 2)) •
      f (circleMap z R x)
have h : ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x *
        (-(circleMap z R x * w * 2) + HPow.hPow (β := ℕ) (circleMap z R x) 2 + HPow.hPow (β := ℕ) w 2)⁻¹ *
      (1 / 2)) •
    f (circleMap z R x) =
  ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x * (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ * (1 / 2)) •
    f (circleMap z R x)
Tactic: rw [inv_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
⊢ ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x *
          (-(circleMap z R x * w * 2) + HPow.hPow (β := ℕ) (circleMap z R x) 2 + HPow.hPow (β := ℕ) w 2)⁻¹ *
        (1 / 2)) •
      f (circleMap z R x) =
    ((↑π : ℂ)⁻¹ * I⁻¹ * deriv (circleMap z R) x * (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ * (1 / 2)) •
      f (circleMap z R x)
have h : -(circleMap z R x * w * 2) + HPow.hPow (β := ℕ) (circleMap z R x) 2 + HPow.hPow (β := ℕ) w 2 =
  HPow.hPow (β := ℕ) (circleMap z R x - w) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0..2 * π, circleTransform R z w f θ =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z)
have simp_rw : ∫ (θ : ℝ) in 0..2 * π,
    (2 * (↑π : ℂ) * I)⁻¹ •
      ((0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) * I) •
        (z + (↑R : ℂ) * cexp ((↑θ : ℂ) * I) - w)⁻¹ • f (z + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) =
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹
    (∫ (θ : ℝ) in 0..2 * π,
      ((0 + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)) * I) •
        (z + (↑R : ℂ) * cexp ((↑θ : ℂ) * I) - w)⁻¹ • f (z + (↑R : ℂ) * cexp ((↑θ : ℂ) * I)))
Tactic: simp_rw [circleTransform, circleIntegral, deriv_circleMap, circleMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransform R z w f)
have hg : Continuous (deriv (circleMap z R))
Tactic: apply_rules [Continuous.smul, continuous_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
hg : Continuous (deriv (circleMap z R))
⊢ Continuous (circleTransform R z w f)
have hg₁ : Continuous (Y := ℂ) fun (x : ℝ) ↦ (circleMap z R x - w)⁻¹
Tactic: apply_rules [Continuous.smul, continuous_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
hg : Continuous (deriv (circleMap z R))
hg₁ : Continuous (Y := ℂ) fun (x : ℝ) ↦ (circleMap z R x - w)⁻¹
⊢ Continuous (circleTransform R z w f)
have hg₂ : Continuous.{0, u_1} (Y := E) fun (x : ℝ) ↦ f (circleMap z R x)
Tactic: apply_rules [Continuous.smul, continuous_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (deriv (circleMap z R))
have hg : Continuous (Y := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I
Tactic: rw [funext <| deriv_circleMap _ _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous.{0, u_1} (Y := E) fun (x : ℝ) ↦ f (circleMap z R x)
have hg : ∀ (x : ℝ), circleMap z R x ∈ sphere z R
Tactic: apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransformDeriv R z w f)
have rw : Continuous.{0, u_1} (Y := E) fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
Tactic: rw [circleTransformDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (circleMap z R w.2 - w.1)⁻¹ 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have simp_rw : ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (1 / (circleMap z R w.2 - w.1)) 2)
  (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: simp_rw [← one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (1 / (circleMap z R w.2 - w.1)) 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have hf : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap z R x.2 - x.1) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
hf : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap z R x.2 - x.1) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (1 / (circleMap z R w.2 - w.1)) 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have hf₁ : ∀ x ∈ SProd.sprod (β := Set ℝ) (closedBall z r) univ, circleMap z R x.2 - x.1 ≠ 0
Tactic: apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0
have ha2 : a ∈ ball z R
Tactic: have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have hg : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ deriv (circleMap z R) x.2) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: apply_rules [ContinuousOn.smul, continuousOn_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
hg :
  ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ deriv (circleMap z R) x.2) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have hg₁ : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ (HPow.hPow (β := ℕ) (circleMap z R x.2 - x.1) 2)⁻¹)
  (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: apply_rules [ContinuousOn.smul, continuousOn_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ deriv (circleMap z R) x.2) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have hg : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap 0 R x.2 * I) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: simp only [deriv_circleMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
have this : ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: have : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ) := by
    apply_rules [ContinuousOn.smul, continuousOn_const]
    · simp only [deriv_circleMap]
      apply_rules [ContinuousOn.mul, (continuous_circleMap 0 R).comp_continuousOn continuousOn_snd,
        continuousOn_const]
    · simpa only [inv_pow] using continuousOn_prod_circle_transform_function hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ∃ (x : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤ ‖circleTransformBoundingFunction R z (↑x : ℂ × ℝ)‖
have cts : ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
  (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
Tactic: have cts := continuousOn_norm_circleTransformBoundingFunction hr z
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts :
  ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ∃ (x : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤ ‖circleTransformBoundingFunction R z (↑x : ℂ × ℝ)‖
have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
Tactic: have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
    apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts :
  ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ (x : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤ ‖circleTransformBoundingFunction R z (↑x : ℂ × ℝ)‖
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
Tactic: have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty :=
    (nonempty_closedBall.2 hr').prod nonempty_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts :
  ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
⊢ ∃ (x : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤ ‖circleTransformBoundingFunction R z (↑x : ℂ × ℝ)‖
have this : ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
  IsMaxOn (β := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
Tactic: have := IsCompact.exists_isMaxOn comp none (cts.mono <| prod_mono_right (subset_univ _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
have obtain : ∀ (r : ℝ) (hr : r < R) (hrx : x ∈ ball z r),
  ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Tactic: obtain ⟨r, hr, hrx⟩ := exists_lt_mem_ball_of_mem_ball hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
have obtain : ∀ (ε' : ℝ) (hε' : ε' > 0) (H : ball x ε' ⊆ ball z r),
  ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Tactic: obtain ⟨ε', hε', H⟩ := exists_ball_subset_ball hrx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
have obtain : ∀ (a : ℂ) (b : ℝ) (ha : (a, b).1 ∈ closedBall z r) (hb : (a, b).2 ∈ [[0, 2 * π]])
  (hab :
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
        ‖circleTransformBoundingFunction R z
            (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) sorry) : ℂ × ℝ)‖),
  ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Tactic: obtain ⟨⟨⟨a, b⟩, ⟨ha, hb⟩⟩, hab⟩ :=
    norm_circleTransformBoundingFunction_le hr (pos_of_mem_ball hrx).le z
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
have obtain : ∀ (X : ℂ) (HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X),
  ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Tactic: obtain ⟨X, -, HX2⟩ := (isCompact_sphere z R).exists_isMaxOn
    (NormedSpace.sphere_nonempty.2 hR.le) hf.norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
have refine : ∀ (y : ℝ) (v : ℂ) (hv : v ∈ ball x ε'), ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
Tactic: refine ⟨‖V b a‖ * ‖f X‖, ε', hε', H.trans (ball_subset_ball hr.le), fun y v hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
have obtain : ∀ (y1 : ℝ) (hy1 : y1 ∈ Ico 0 (2 * π)) (hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1),
  ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
Tactic: obtain ⟨y1, hy1, hfun⟩ :=
    Periodic.exists_mem_Ico₀ (circleTransformDeriv_periodic R z v f) Real.two_pi_pos y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
have hy2 : y1 ∈ [[0, 2 * π]]
Tactic: have hy2 : y1 ∈ [[0, 2 * π]] := Icc_subset_uIcc <| Ico_subset_Icc_self hy1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
have HX2₁ : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
Tactic: simp only [isMaxOn_iff, mem_sphere_iff_norm] at HX2
Cleared hypotheses: HX2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (hypothesis)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
have this : ‖circleTransformBoundingFunction R z
        (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (v, y1) sorry) : ℂ × ℝ)‖ *
    ‖f (circleMap z R y1)‖ ≤
  ‖circleTransformBoundingFunction R z
        (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) sorry) : ℂ × ℝ)‖ *
    ‖f X‖
Tactic: have := mul_le_mul (hab ⟨⟨v, y1⟩, ⟨ball_subset_closedBall (H hv), hy2⟩⟩)
    (HX2 (circleMap z R y1) (mem_sphere_iff_norm.1 (circleMap_mem_sphere z hR.le y1)))
    (norm_nonneg _) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CircleTransform (goal)
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (v, y1) ⋯) : ℂ × ℝ)‖ *
      ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖ *
      ‖f X‖
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
have rw : ‖circleTransformDeriv R z v f y1‖ ≤ ‖V b a‖ * ‖f X‖
Tactic: rw [hfun]