awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - a‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖)

Tactic:
simp [mul_sub, circleMap, add_mul, Complex.exp_add]

Premises used: add_mul, Complex.exp_add, mul_sub, circleMap
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ a ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)

Tactic:
simp [← hζ, inv_mul_cancel₀ (by aesop : a ≠ 0)]

Premises used: inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖) (x + 2 * π)) ((fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖) x)

Tactic:
simp [periodic_circleMap 0 1 x]

Premises used: periodic_circleMap, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Function.Periodic (β := ℝ) (fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)

Tactic:
have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
this : Function.Periodic (β := ℝ) (fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..0 + 2 * π, log ‖circleMap 0 1 x - 1‖)
    (∫ (x : ℝ) in ζ..ζ + 2 * π, log ‖circleMap 0 1 x - 1‖)

Tactic:
have := this.intervalIntegral_add_eq (t := 0) (s := ζ)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
this_1 : Function.Periodic (β := ℝ) (fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)
this :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..0 + 2 * π, log ‖circleMap 0 1 x - 1‖)
    (∫ (x : ℝ) in ζ..ζ + 2 * π, log ‖circleMap 0 1 x - 1‖)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)

Tactic:
simp_all [integral_comp_add_left (log ‖circleMap 0 1 · - 1‖)]

Premises used: Norm.norm, HSub.hSub, circleMap, Real.log, intervalIntegral.integral_comp_add_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
h₁ :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖)
    (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) [[0, 2 * π]]
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)

Tactic:
apply integral_congr

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
h₁ : log ((Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1)) / 2 = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2
⊢ log ‖circleMap 0 1 x - 1‖ = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2

Tactic:
rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg]

Premises used: Real.log_sqrt, HSub.hSub, circleMap, Complex.norm_def, Complex.normSq_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
h₁ : (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
⊢ log ((Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1)) / 2 = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = (cos x - 1) * (cos x - 1) + sin x * sin x

Tactic:
simp [circleMap, Complex.normSq_apply]

Premises used: circleMap, Complex.normSq_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ (cos x - 1) * (cos x - 1) + sin x * sin x =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
rw : HAdd.hAdd (α := ℝ) 1 1 - 2 * cos x = 2 - 2 * cos x
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x = 2 - 2 * cos x

Tactic:
rw [sin_sq_add_cos_sq]

Premises used: Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ HAdd.hAdd (α := ℝ) 1 1 - 2 * cos x = 2 - 2 * cos x

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
rw : 2 - 2 * cos x = 2 - 2 * cos (2 * x / 2)
⊢ 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 2))

Tactic:
rw [← mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 2 - 2 * cos x = 2 - 2 * cos (2 * x / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
rw : 2 - 2 * (2 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 - 1) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2
⊢ 2 - 2 * cos (2 * (x / 2)) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2

Tactic:
rw [cos_two_mul]

Premises used: Real.cos_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 2 - 2 * (2 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 - 1) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
nth_rw :
  4 * (HPow.hPow (β := ℕ) (sin (x / 2)) 2 + HPow.hPow (β := ℕ) (cos (x / 2)) 2) -
      4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 =
    4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
⊢ 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2

Tactic:
nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]

Premises used: HDiv.hDiv, Real.sin_sq_add_cos_sq, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 * (HPow.hPow (β := ℕ) (sin (x / 2)) 2 + HPow.hPow (β := ℕ) (cos (x / 2)) 2) -
      4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 =
    4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
calc : (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = (cos x - 1) * (cos x - 1) + sin x * sin x
calc₁ :
  (cos x - 1) * (cos x - 1) + sin x * sin x =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x
calc₂ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x = 2 - 2 * cos x
calc₃ : 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 2))
calc₄ : 2 - 2 * cos (2 * (x / 2)) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2
calc₅ : 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2

Tactic:
calc Complex.normSq (circleMap 0 1 x - 1)
    _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
      simp [circleMap, Complex.normSq_apply]
    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
      ring
    _ = 2 - 2 * cos x := by
      rw [sin_sq_add_cos_sq]
      norm_num
    _ = 2 - 2 * cos (2 * (x / 2)) := by
      rw [← mul_div_assoc]
      simp
    _ = 4 - 4 * cos (x / 2) ^ 2 := by
      rw [cos_two_mul]
      ring
    _ = 4 * sin (x / 2) ^ 2 := by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring

Premises used: HMul.hMul, Real.cos, HSub.hSub, circleMap, HDiv.hDiv, Complex.normSq, OfNat.ofNat, DFunLike.coe, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0

Tactic:
circleAverage_log_norm_sub_const₁_integral

Premises used: _private.0.circleAverage_log_norm_sub_const₁_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
calc :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - a‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖)
calc₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖)
calc₂ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)
calc₃ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
calc₄ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0

Tactic:
calc ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - a‖
  _ = ∫ x in 0..(2 * π), log ‖(circleMap 0 1 ζ) * (circleMap 0 1 x - a)‖ := by
    simp
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - (circleMap 0 1 ζ) * a‖ := by
    simp [mul_sub, circleMap, add_mul, Complex.exp_add]
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - 1‖ := by
    simp [← hζ, inv_mul_cancel₀ (by aesop : a ≠ 0)]
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - 1‖ := by
    have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
    have := this.intervalIntegral_add_eq (t := 0) (s := ζ)
    simp_all [integral_comp_add_left (log ‖circleMap 0 1 · - 1‖)]
  _ = ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 := by
    apply integral_congr
    intro x hx
    simp only []
    rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg]
    congr
    calc Complex.normSq (circleMap 0 1 x - 1)
    _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
      simp [circleMap, Complex.normSq_apply]
    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
      ring
    _ = 2 - 2 * cos x := by
      rw [sin_sq_add_cos_sq]
      norm_num
    _ = 2 - 2 * cos (2 * (x / 2)) := by
      rw [← mul_div_assoc]
      simp
    _ = 4 - 4 * cos (x / 2) ^ 2 := by
      rw [cos_two_mul]
      ring
    _ = 4 * sin (x / 2) ^ 2 := by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring
  _ = 0 := circleAverage_log_norm_sub_const₁_integral

Premises used: Real.pi, HMul.hMul, _private.0.circleAverage_log_norm_sub_const₁_integral, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
rw : InnerProductSpace.HarmonicOnNhd (F := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) (closedBall 0 |1|)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log ‖a‖

Tactic:
rw [HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg]

Premises used: HarmonicOnNhd.circleAverage_eq, norm_neg, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x - a) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
apply : x - a ≠ 0
⊢ InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) x

Tactic:
apply AnalyticAt.harmonicAt_log_norm (by fun_prop)

Premises used: AnalyticAt.harmonicAt_log_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
rw : x ≠ a
⊢ x - a ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
by_contra! : ∀ (this : x = a), False
⊢ x ≠ a

Tactic:
by_contra!
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : x = a
⊢ ‖a‖ ≤ 1

Tactic:
simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right]

Premises used: Metric.mem_closedBall, abs_one, dist_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : x = a
hx₁ : ‖a‖ ≤ 1
⊢ x = a

Tactic:
simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right]

Premises used: Metric.mem_closedBall, abs_one, dist_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : ‖a‖ ≤ 1
this : x = a
linarith : 1 - ‖a‖ + (‖a‖ - 1) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
inl : ∀ (h : 1 < ‖a‖), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
inr : ∀ (h : 1 = ‖a‖), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
inr₁ : ∀ (h : ‖a‖ < 1), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rcases lt_trichotomy 1 ‖a‖ with h | h | h

Premises used: Norm.norm, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
inl : log ‖a‖ = log⁺ ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rw [circleAverage_log_norm_sub_const₂ h]

Premises used: circleAverage_log_norm_sub_const₂
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
apply : 1 ≤ |‖a‖|
⊢ log ‖a‖ = log⁺ ‖a‖

Tactic:
apply (posLog_eq_log _).symm

Premises used: Real.posLog_eq_log, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 < ‖a‖
⊢ 1 ≤ |‖a‖|

Tactic:
simp_all [le_of_lt h]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 = ‖a‖
inr : |‖a‖| ≤ 1
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]

Premises used: circleAverage_log_norm_sub_const₁, Real.posLog_eq_zero_iff, eq_comm, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : 1 = ‖a‖
⊢ |‖a‖| ≤ 1

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
inr : |‖a‖| ≤ 1
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rw [eq_comm, circleAverage_log_norm_sub_const₀ h, posLog_eq_zero_iff]

Premises used: circleAverage_log_norm_sub_const₀, Real.posLog_eq_zero_iff, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
⊢ |‖a‖| ≤ 1

Tactic:
simp_all [le_of_lt h]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
⊢ Eq (α := ℂ → ℝ) (fun (x : ℂ) ↦ log ‖x + a‖) fun (x : ℂ) ↦ log ‖x - -a‖

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
⊢ Eq (α := ℂ → ℝ) (fun (x : ℂ) ↦ log ‖x + a‖) fun (x : ℂ) ↦ log ‖x - -a‖

Tactic:
have : (log ‖· + a‖) = (log ‖· - -a‖) := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
this : Eq (α := ℂ → ℝ) (fun (x : ℂ) ↦ log ‖x + a‖) fun (x : ℂ) ↦ log ‖x - -a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x + a‖) 0 1 = log⁺ ‖a‖

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
rw :
  Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)

Tactic:
rw [circleAverage_eq_circleAverage_zero_one]

Premises used: Real.circleAverage_eq_circleAverage_zero_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
e_f :
  Eq (α := ℂ → ℝ) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
⊢ Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
e_f : ∀ (z : ℂ), log ‖(↑R : ℂ) * z + c - a‖ = log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
⊢ Eq (α := ℂ → ℝ) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖

Tactic:
ext z
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
e_f : (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))
⊢ log ‖(↑R : ℂ) * z + c - a‖ = log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
e_f : (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R : ℂ)⁻¹ * (c - a))
⊢ (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))

Tactic:
rw [Complex.ofReal_inv R]

Premises used: Complex.ofReal_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R : ℂ)⁻¹ * (c - a))

Tactic:
field [Complex.ofReal_ne_zero.mpr hR]

Premises used: Iff.mpr, Complex.ofReal_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
apply :
  EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖)
    fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
⊢ Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)

Tactic:
apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm

Premises used: Real, Ne.symm, Real.circleAverage_congr_codiscreteWithin, zero_ne_one'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
apply :
  ∀ (z : ℂ),
    Membership.mem (γ := Set ℂ) (sphere 0 |1|) z →
      ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0})).Finite
⊢ Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}

Tactic:
apply codiscreteWithin_iff_locallyFiniteComplementWithin.2

Premises used: Iff.mpr, codiscreteWithin_iff_locallyFiniteComplementWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
h : Set.univ ∈ nhds z ∧ Set.Finite (α := ℂ) (Set.univ ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}))
⊢ ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0})).Finite

Tactic:
use Set.univ

Premises used: Set.univ
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
h : Set.Finite (α := ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0})
⊢ Set.univ ∈ nhds z ∧ Set.Finite (α := ℂ) (Set.univ ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}))

Tactic:
simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]

Premises used: norm_eq_zero, Set.univ_inter, ne_eq, abs_one, Filter.univ_mem, Complex.ofReal_inv, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
h : Set.Subsingleton (α := ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0})
⊢ Set.Finite (α := ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0})

Tactic:
apply Set.Subsingleton.finite

Premises used: Set.Subsingleton.finite
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
z₁ : ℂ
hz₁ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₁
z₂ : ℂ
hz₂ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₂
⊢ ¬R = 0

Tactic:
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]

Premises used: sub_zero, Set.mem_setOf_eq, ne_eq, mem_sphere_iff_norm, Set.mem_diff, Decidable.not_not, abs_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
z₁ : ℂ
hz₁ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₁
z₂ : ℂ
hz₂ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₂
hR₁ : ¬R = 0
⊢ ‖z‖ = 1

Tactic:
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]

Premises used: sub_zero, Set.mem_setOf_eq, ne_eq, mem_sphere_iff_norm, Set.mem_diff, Decidable.not_not, abs_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
z₁ : ℂ
hz₁ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₁
z₂ : ℂ
hz₂ : Membership.mem (γ := Set ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0}) z₂
hR₁ : ¬R = 0
hz₃ : ‖z‖ = 1
⊢ ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0

Tactic:
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]

Premises used: sub_zero, Set.mem_setOf_eq, ne_eq, mem_sphere_iff_norm, Set.mem_diff, Decidable.not_not, abs_one