awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleIntegral
Goal:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) 0
this : ∮ (z : ℂ) in C(c, R), HPow.hPow (β := ℕ) ((w - c) / (z - c)) 0 * (z - c)⁻¹ = 2 * (↑π : ℂ) * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz : z ∈ sphere c R
rw : (z - c)⁻¹ ^ (n + 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₁ : HPow.hPow (β := ℤ) (z - c)⁻¹ (↑(n + 1) : ℤ) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₂ : (HPow.hPow (β := ℤ) (z - c) (↑(n + 1) : ℤ))⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₃ : HPow.hPow (β := ℤ) (z - c) (-(↑(n + 1) : ℤ)) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₄ : (z - c) ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₅ : (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
rw₆ rw₇ : (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) = (z - c) ^ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1)
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]

Premises used: zpow_natCast, pow_succ, sub_eq_add_neg, inv_zpow, neg_add, Int.natCast_succ, zpow_neg, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)

Tactic:
have := periodic_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
simp_rw :
  (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) (x + 2 * π) • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) x • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x)
⊢ circleTransformDeriv R z w f (x + 2 * π) = circleTransformDeriv R z w f x

Tactic:
simp_rw [circleTransformDeriv, this]

Premises used: Complex.circleTransformDeriv
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
e_a : deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x
⊢ (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) (x + 2 * π) • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      deriv (circleMap z R) x • (HPow.hPow (β := ℕ) (circleMap z R x - w) 2)⁻¹ • f (circleMap z R x)

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
this : ∀ (c : ℂ) (R x : ℝ), circleMap c R (x + 2 * π) = circleMap c R x
x : ℝ
⊢ deriv (circleMap z R) (x + 2 * π) = deriv (circleMap z R) x

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
h : ∀ (x : ℝ), circleTransformDeriv R z w f x = (circleMap z R x - w)⁻¹ • circleTransform R z w f x
⊢ circleTransformDeriv R z w f = fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
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)
⊢ circleTransformDeriv R z w f x = (circleMap z R x - w)⁻¹ • circleTransform R z w f x

Tactic:
simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]

Premises used: mul_assoc, Complex.circleTransform, Complex.circleTransformDeriv, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
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)
⊢ ((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:
ring_nf
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
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)
⊢ ((↑π : ℂ)⁻¹ * 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]

Premises used: inv_pow
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
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
⊢ ((↑π : ℂ)⁻¹ * 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:
congr
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x : ℝ
⊢ -(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:
ring
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
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)))
⊢ ∫ (θ : ℝ) in 0..2 * π, circleTransform R z w f θ =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z)

Tactic:
simp_rw [circleTransform, circleIntegral, deriv_circleMap, circleMap]

Premises used: circleMap, deriv_circleMap, Complex.circleTransform, circleIntegral
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) 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
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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)⁻¹
hg₂ : Continuous.{0, u_1} (Y := E) fun (x : ℝ) ↦ f (circleMap z R x)
⊢ Continuous (circleTransform R z w f)

Tactic:
apply_rules [Continuous.smul, continuous_const]

Premises used: continuous_const, Continuous.smul
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (Y := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I
⊢ Continuous (deriv (circleMap z R))

Tactic:
rw [funext <| deriv_circleMap _ _]

Premises used: deriv_circleMap, funext
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (Y := ℂ) fun (x : ℝ) ↦ circleMap 0 R x * I

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (Y := ℂ) fun (x : ℝ) ↦ (circleMap z R x - w)⁻¹

Tactic:
continuous_circleMap_inv hw

Premises used: continuous_circleMap_inv
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (Y := ℂ) fun (x : ℝ) ↦ (circleMap z R x - w)⁻¹

Tactic:
exact continuous_circleMap_inv hw

Premises used: continuous_circleMap_inv
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 : ∀ (x : ℝ), circleMap z R x ∈ sphere z R
⊢ Continuous.{0, u_1} (Y := E) fun (x : ℝ) ↦ f (circleMap z R x)

Tactic:
apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)

Premises used: ContinuousOn.comp_continuous, continuous_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R

Tactic:
fun _ => (circleMap_mem_sphere _ hR.le) _

Premises used: LT.lt.le, circleMap_mem_sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R

Tactic:
exact fun _ => (circleMap_mem_sphere _ hR.le) _

Premises used: LT.lt.le, circleMap_mem_sphere
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
rw : Continuous.{0, u_1} (Y := E) fun (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
⊢ Continuous (circleTransformDeriv R z w f)

Tactic:
rw [circleTransformDeriv_eq]

Premises used: Complex.circleTransformDeriv_eq
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ

Tactic:
(continuous_circleMap_inv hw).smul (continuous_circleTransform hR hf hw)

Premises used: Complex.continuous_circleTransform, Continuous.smul, continuous_circleMap_inv
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 (θ : ℝ) ↦ (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ

Tactic:
exact (continuous_circleMap_inv hw).smul (continuous_circleTransform hR hf hw)

Premises used: Complex.continuous_circleTransform, Continuous.smul, continuous_circleMap_inv
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
simp_rw :
  ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (1 / (circleMap z R w.2 - w.1)) 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (circleMap z R w.2 - w.1)⁻¹ 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
simp_rw [← one_div]

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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)
hf₁ : ∀ x ∈ SProd.sprod (β := Set ℝ) (closedBall z r) univ, circleMap z R x.2 - x.1 ≠ 0
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ × ℝ) ↦ HPow.hPow (β := ℕ) (1 / (circleMap z R w.2 - w.1)) 2)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]

Premises used: continuousOn_const, ContinuousOn.div, ContinuousOn.pow
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap z R x.2 - x.1) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst

Premises used: Continuous.comp_continuousOn, ContinuousOn.sub, continuous_circleMap, continuousOn_snd, continuousOn_fst
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap z R x.2 - x.1) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
exact ((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst

Premises used: Continuous.comp_continuousOn, ContinuousOn.sub, continuous_circleMap, continuousOn_snd, continuousOn_fst
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
⊢ a ∈ ball z R

Tactic:
have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
ha2 : a ∈ ball z R
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Tactic:
sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)

Premises used: Iff.mpr, sub_ne_zero, circleMap_ne_mem_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
ha2 : a ∈ ball z R
⊢ circleMap z R (a, b).2 - (a, b).1 ≠ 0

Tactic:
exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)

Premises used: Iff.mpr, sub_ne_zero, circleMap_ne_mem_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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)
hg₁ :
  ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ (HPow.hPow (β := ℕ) (circleMap z R x.2 - x.1) 2)⁻¹)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
apply_rules [ContinuousOn.smul, continuousOn_const]

Premises used: continuousOn_const, ContinuousOn.smul
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
hg : ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap 0 R x.2 * I) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ deriv (circleMap z R) x.2) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
simp only [deriv_circleMap]

Premises used: deriv_circleMap
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ circleMap 0 R x.2 * I) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
apply_rules [ContinuousOn.mul, (continuous_circleMap 0 R).comp_continuousOn continuousOn_snd,
        continuousOn_const]

Premises used: Continuous.comp_continuousOn, continuousOn_const, continuous_circleMap, continuousOn_snd, OfNat.ofNat, ContinuousOn.mul
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ × ℝ) ↦ (HPow.hPow (β := ℕ) (circleMap z R x.2 - x.1) 2)⁻¹)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
simpa only [inv_pow] using continuousOn_prod_circle_transform_function hr

Premises used: inv_pow, Complex.continuousOn_prod_circle_transform_function
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
this.norm

Premises used: ContinuousOn.norm
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (SProd.sprod (β := Set ℝ) (closedBall z r) univ)
⊢ ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
exact this.norm

Premises used: ContinuousOn.norm
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ContinuousOn (Y := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z)
    (SProd.sprod (β := Set ℝ) (closedBall z r) univ)

Tactic:
have cts := continuousOn_norm_circleTransformBoundingFunction hr z
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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)
⊢ IsCompact (closedBall z r ×ˢ [[0, 2 * π]])

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

Premises used: IsCompact.prod, isCompact_uIcc, ProperSpace.isCompact_closedBall
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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)
⊢ 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]
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 * π]])
⊢ (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty

Tactic:
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty :=
    (nonempty_closedBall.2 hr').prod nonempty_uIcc
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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 * π]],
    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 _))
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn (β := ℝ) ((fun (x : ℂ) ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ (x : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
      ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤ ‖circleTransformBoundingFunction R z (↑x : ℂ × ℝ)‖

Tactic:
simpa [isMaxOn_iff] using this

Premises used: isMaxOn_iff
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
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
⊢ ∃ (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

Premises used: Metric.exists_lt_mem_ball_of_mem_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
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
⊢ ∃ (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

Premises used: Metric.exists_ball_subset_ball
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
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
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) ⋯) : ℂ × ℝ)‖),
    ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
⊢ ∃ (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

Premises used: Complex.norm_circleTransformBoundingFunction_le, LT.lt.le, Metric.pos_of_mem_ball