awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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))
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have calc₄ : 2 - 2 * cos (2 * (x / 2)) = 4 - 4 * HPow.hPow (β := ℕ) (cos (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have calc₅ : 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 = 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have 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)‖)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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)‖)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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‖)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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‖)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have calc₃ : Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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‖)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log ‖a‖
have rw : InnerProductSpace.HarmonicOnNhd (F := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) (closedBall 0 |1|)
Tactic: rw [HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) x
have apply : x - a ≠ 0
Tactic: apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ x - a ≠ 0
have rw : x ≠ a
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : x = a
⊢ False
have hx₁ : ‖a‖ ≤ 1
Tactic: simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right]
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : ‖a‖ ≤ 1
this : x = a
⊢ False
have linarith : 1 - ‖a‖ + (‖a‖ - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inl : ∀ (h : 1 < ‖a‖), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
Tactic: rcases lt_trichotomy 1 ‖a‖ with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
inl : ∀ (h : 1 < ‖a‖), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inr : ∀ (h : 1 = ‖a‖), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
Tactic: rcases lt_trichotomy 1 ‖a‖ with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inr₁ : ∀ (h : ‖a‖ < 1), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
Tactic: rcases lt_trichotomy 1 ‖a‖ with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inl : log ‖a‖ = log⁺ ‖a‖
Tactic: rw [circleAverage_log_norm_sub_const₂ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 < ‖a‖
⊢ log ‖a‖ = log⁺ ‖a‖
have apply : 1 ≤ |‖a‖|
Tactic: apply (posLog_eq_log _).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : 1 = ‖a‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inr : |‖a‖| ≤ 1
Tactic: rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖
have inr : |‖a‖| ≤ 1
Tactic: rw [eq_comm, circleAverage_log_norm_sub_const₀ h, posLog_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x + a‖) 0 1 = log⁺ ‖a‖
have this : Eq (α := ℂ → ℝ) (fun (x : ℂ) ↦ log ‖x + a‖) fun (x : ℂ) ↦ log ‖x - -a‖
Tactic: have : (log ‖· + a‖) = (log ‖· - -a‖) := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
have rw : Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) 0 1)
  (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
Tactic: rw [circleAverage_eq_circleAverage_zero_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
have e_f : Eq (α := ℂ → ℝ) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Eq (α := ℂ → ℝ) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * z + c - a‖) fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
have e_f : ∀ (z : ℂ), log ‖(↑R : ℂ) * z + c - a‖ = log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ log ‖(↑R : ℂ) * z + c - a‖ = log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖
have e_f : (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))
have e_f : (↑R : ℂ) * z + c - a = (↑R : ℂ) * (z + (↑R : ℂ)⁻¹ * (c - a))
Tactic: rw [Complex.ofReal_inv R]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)
have apply : EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖)
  fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
Tactic: apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
have apply : ∀ (z : ℂ),
  Membership.mem (γ := Set ℂ) (sphere 0 |1|) z →
    ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0})).Finite
Tactic: apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
⊢ ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0})).Finite
have h : Set.univ ∈ nhds z ∧ Set.Finite (α := ℂ) (Set.univ ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}))
Tactic: use Set.univ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
⊢ Set.univ ∈ nhds z ∧ Set.Finite (α := ℂ) (Set.univ ∩ (sphere 0 |1| \ {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}))
have h : Set.Finite (α := ℂ) (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
⊢ Set.Finite (α := ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0})
have h : Set.Subsingleton (α := ℂ) (sphere 0 1 \ {z : ℂ | ¬z + (↑R : ℂ)⁻¹ * (c - a) = 0})
Tactic: apply Set.Subsingleton.finite
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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₂
⊢ z₁ = z₂
have hR₁ : ¬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]
Cleared hypotheses: hR, hz, hz₁, hz₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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₁ = z₂
have hz₃ : ‖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]
Cleared hypotheses: hR, hz, hz₁, hz₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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₁ = z₂
have hz₄ : ‖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]
Cleared hypotheses: hR, hz, hz₁, hz₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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
hz₄ : ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0
⊢ z₁ = z₂
have hz₅ : ‖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]
Cleared hypotheses: hR, hz, hz₁, hz₂