awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₀ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₂ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₁₃ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₀ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₂ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 2 1 = 2
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₁₄ : -(log 2 * π) / 2 < -(π / 2 * log 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₀ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
linarith₁₂ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₄ : -(log 2 * π) / 2 < -(π / 2 * log 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₁₅ : -(log 2 * π) / 2 < -(π / 2 * log 2) → -(1 * log 2 * (1 * π)) - -(1 * π * (1 * log 2)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
have calc : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))
Tactic: calc ∫ x in 0..(π / 2), log (sin x)
    _ = ∫ x in 0..(π / 2), (log (sin (2 * x)) - log 2 - log (cos x)) := by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring
    _ = (∫ x in 0..(π / 2), log (sin (2 * x))) - π / 2 * log 2
        - ∫ x in 0..(π / 2), log (cos x) := by
      rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
      · simp
      · simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · exact intervalIntegrable_log_cos
    _ = (∫ x in 0..(π / 2), log (sin (2 * x)))
        - π / 2 * log 2 - ∫ x in 0..(π / 2), log (sin x) := by
      simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
    _ = -log 2 * π / 2 := by
      simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]
      linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
calc : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))
⊢ ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
have calc₁ : ∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x) =
  (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)
Tactic: calc ∫ x in 0..(π / 2), log (sin x)
    _ = ∫ x in 0..(π / 2), (log (sin (2 * x)) - log 2 - log (cos x)) := by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring
    _ = (∫ x in 0..(π / 2), log (sin (2 * x))) - π / 2 * log 2
        - ∫ x in 0..(π / 2), log (cos x) := by
      rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
      · simp
      · simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · exact intervalIntegrable_log_cos
    _ = (∫ x in 0..(π / 2), log (sin (2 * x)))
        - π / 2 * log 2 - ∫ x in 0..(π / 2), log (sin x) := by
      simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
    _ = -log 2 * π / 2 := by
      simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]
      linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
calc : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))
calc₁ :
  ∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)
⊢ ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
have calc₂ : (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
  (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x)
Tactic: calc ∫ x in 0..(π / 2), log (sin x)
    _ = ∫ x in 0..(π / 2), (log (sin (2 * x)) - log 2 - log (cos x)) := by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring
    _ = (∫ x in 0..(π / 2), log (sin (2 * x))) - π / 2 * log 2
        - ∫ x in 0..(π / 2), log (cos x) := by
      rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
      · simp
      · simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · exact intervalIntegrable_log_cos
    _ = (∫ x in 0..(π / 2), log (sin (2 * x)))
        - π / 2 * log 2 - ∫ x in 0..(π / 2), log (sin x) := by
      simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
    _ = -log 2 * π / 2 := by
      simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]
      linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
calc : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))
calc₁ :
  ∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)
calc₂ :
  (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x)
⊢ ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
have calc₃ : (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
Tactic: calc ∫ x in 0..(π / 2), log (sin x)
    _ = ∫ x in 0..(π / 2), (log (sin (2 * x)) - log 2 - log (cos x)) := by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring
    _ = (∫ x in 0..(π / 2), log (sin (2 * x))) - π / 2 * log 2
        - ∫ x in 0..(π / 2), log (cos x) := by
      rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
      · simp
      · simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · exact intervalIntegrable_log_cos
    _ = (∫ x in 0..(π / 2), log (sin (2 * x)))
        - π / 2 * log 2 - ∫ x in 0..(π / 2), log (sin x) := by
      simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
    _ = -log 2 * π / 2 := by
      simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]
      linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ ∫ (x : ℝ) in 0..π, log (sin x) = -log 2 * π
have rw : 2 * (-log 2 * π / 2) = -log 2 * π
Tactic: rw [integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two,
    integral_log_sin_zero_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1)
have hf : Set.EqOn (β := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) (sphere 0 |1|)
Tactic: apply circleAverage_congr_sphere
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
⊢ Eq (α := ℝ) ((fun (x : ℂ) ↦ log ‖x - a‖) z) ((fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) z)
have hz₁ : ‖z‖ = 1
Tactic: simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
⊢ log ‖z - a‖ = log ‖1 - z⁻¹ * a‖
have hf : ‖z - a‖ = ‖1 - z⁻¹ * a‖
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
⊢ ‖z - a‖ = ‖1 - z⁻¹ * a‖
have this : z ≠ 0
Tactic: have : z ≠ 0 := fun h ↦ by simp [h] at hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
⊢ ‖z - a‖ = ‖1 - z⁻¹ * a‖
have calc : ‖z - a‖ = ‖z⁻¹ * (z - a)‖
Tactic: calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
calc : ‖z - a‖ = ‖z⁻¹ * (z - a)‖
⊢ ‖z - a‖ = ‖1 - z⁻¹ * a‖
have calc₁ : ‖z⁻¹ * (z - a)‖ = ‖1 - z⁻¹ * a‖
Tactic: calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1) 0
have rw : InnerProductSpace.HarmonicOnNhd (F := ℝ) (fun (x : ℂ) ↦ log ‖1 - x * a‖) (closedBall 0 |1|)
Tactic: rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ ‖x * a‖ < 1
have calc : ‖x * a‖ = ‖x‖ * ‖a‖
Tactic: calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖1 - x * a‖) x
have this : ‖x * a‖ < 1
Tactic: have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
⊢ InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖1 - x * a‖) x
have apply : 1 - 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 : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
⊢ 1 - x * a ≠ 0
have rw : 1 ≠ x * a
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
hCon : 1 = x * a
⊢ False
have rwa : ∀ (this : Norm.norm (E := ℂ) 1 < 1) (hCon : 1 = x * a), False
Tactic: rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
Cleared hypotheses: this, hCon
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
hCon : 1 = x * a
rwa : ∀ (this : Norm.norm (E := ℂ) 1 < 1) (hCon : 1 = x * a), False
⊢ False
have rwa₁ : ∀ (this : LT.lt (α := ℝ) 1 1) (hCon : 1 = x * a), False
Tactic: rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
Cleared hypotheses: this, hCon
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
hCon : 1 = x * a
rwa : ∀ (this : Norm.norm (E := ℂ) 1 < 1) (hCon : 1 = x * a), False
rwa₁ : ∀ (this : LT.lt (α := ℝ) 1 1) (hCon : 1 = x * a), False
⊢ False
have rwa₂ : ∀ (this : False) (hCon : 1 = x * a), False
Tactic: rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
Cleared hypotheses: this, hCon
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) 0
have calc : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1)
Tactic: calc circleAverage (log ‖· - a‖) 0 1
  _ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 := by
    apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
  _ = 0 := by
    rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
    intro x hx
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
    apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
    rw [sub_ne_zero]
    by_contra! hCon
    rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ < 1
calc : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1)
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) 0
have calc₁ : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1) 0
Tactic: calc circleAverage (log ‖· - a‖) 0 1
  _ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 := by
    apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
  _ = 0 := by
    rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
    intro x hx
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
    apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
    rw [sub_ne_zero]
    by_contra! hCon
    rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)
    (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2))
have this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
Tactic: have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)
    (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2))
have rw : Eq (α := ℝ) (∫ (x : ℝ) in 0 / 2..2 * π / 2, log (4 * HPow.hPow (β := ℕ) (sin x) 2))
  (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2))
Tactic: rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2)) (∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x))
have hf : (codiscreteWithin (Ι 0 π)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin x) 2)) fun (x : ℝ) ↦
  log 4 + 2 * log (sin x)
Tactic: apply integral_congr_codiscreteWithin
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ Ι 0 π ⊆ Set.univ
have tauto : ∀ ⦃a : ℝ⦄, a ∈ Ι 0 π → Membership.mem (γ := Set ℝ) Set.univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ (codiscreteWithin (Ι 0 π)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin x) 2)) fun (x : ℝ) ↦
    log 4 + 2 * log (sin x)
have hf : Membership.mem (γ := Filter ℝ) (codiscreteWithin Set.univ)
  {x : ℝ |
    (fun (x : ℝ) ↦
        Eq (α := ℝ) ((fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin x) 2)) x)
          ((fun (x : ℝ) ↦ log 4 + 2 * log (sin x)) x))
      x}
Tactic: apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)