awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
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
linarith₁₅ : -(log 2 * π) / 2 < -(π / 2 * log 2) → -(1 * log 2 * (1 * π)) - -(1 * π * (1 * log 2)) = 0
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
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)
calc₃ : (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 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

Premises used: Real.pi, HMul.hMul, intervalIntegral, HDiv.hDiv, Real.log, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
rw : 2 * (-log 2 * π / 2) = -log 2 * π
⊢ ∫ (x : ℝ) in 0..π, log (sin x) = -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]

Premises used: integral_log_sin_zero_pi_div_two, _private.0.integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ 2 * (-log 2 * π / 2) = -log 2 * π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a c : ℂ
r : ℝ
z : ℂ
hz : z ∈ sphere c |r|
⊢ MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ x - a) z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
hf : Set.EqOn (β := ℝ) (fun (x : ℂ) ↦ log ‖x - a‖) (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) (sphere 0 |1|)
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1)

Tactic:
apply circleAverage_congr_sphere

Premises used: Real.circleAverage_congr_sphere
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |1|) z
⊢ ‖z‖ = 1

Tactic:
simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]

Premises used: sub_zero, mem_sphere_iff_norm, abs_one
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
hf : ‖z - a‖ = ‖1 - z⁻¹ * a‖
⊢ log ‖z - a‖ = log ‖1 - z⁻¹ * a‖

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h_1 : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
h : z = 0
⊢ False

Tactic:
simp [h] at hz
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
⊢ z ≠ 0

Tactic:
have : z ≠ 0 := fun h ↦ by simp [h] at hz
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
⊢ ‖z - a‖ = ‖z⁻¹ * (z - a)‖

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
⊢ ‖z⁻¹ * (z - a)‖ = ‖1 - z⁻¹ * a‖

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
calc : ‖z - a‖ = ‖z⁻¹ * (z - a)‖
calc₁ : ‖z⁻¹ * (z - a)‖ = ‖1 - z⁻¹ * a‖
⊢ ‖z - a‖ = ‖1 - z⁻¹ * a‖

Tactic:
calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
rw : InnerProductSpace.HarmonicOnNhd (F := ℝ) (fun (x : ℂ) ↦ log ‖1 - x * a‖) (closedBall 0 |1|)
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1) 0

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]

Premises used: CStarRing.norm_of_mem_unitary, HarmonicOnNhd.circleAverage_eq, sub_zero, unitary, MulZeroClass.zero_mul, Real.log_one, Submonoid.one_mem, Real.circleAverage_zero_one_congr_inv, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ ‖x * a‖ = ‖x‖ * ‖a‖

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

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

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

Tactic:
calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h

Premises used: mul_le_of_le_one_left, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
⊢ ‖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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closedBall 0 |1|) x
this : ‖x * a‖ < 1
⊢ AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ 1 - x * a) x

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

Tactic:
rw [sub_ne_zero]

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

Tactic:
by_contra! hCon
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : False) (hCon : 1 = x * a), False
⊢ False

Tactic:
rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this

Premises used: CStarRing.norm_of_mem_unitary, unitary, Submonoid.one_mem, lt_self_iff_false, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ < 1
calc : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1)
calc₁ : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖1 - x⁻¹ * a‖) 0 1) 0
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖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

Premises used: Norm.norm, HMul.hMul, HSub.hSub, Real.log, Inv.inv, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
x : ℝ
⊢ x / 2 = 2⁻¹ * x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
⊢ ∀ {x : ℝ}, x / 2 = 2⁻¹ * x

Tactic:
have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
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))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 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))]

Premises used: intervalIntegral.integral_div, intervalIntegral.inv_mul_integral_comp_div
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
⊢ 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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
hf :
  (codiscreteWithin (Ι 0 π)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin x) 2)) fun (x : ℝ) ↦
    log 4 + 2 * log (sin x)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2)) (∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x))

Tactic:
apply integral_congr_codiscreteWithin

Premises used: intervalIntegral.integral_congr_codiscreteWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ ⦃a : ℝ⦄, a ∈ Ι 0 π → Membership.mem (γ := Set ℝ) Set.univ a
⊢ Ι 0 π ⊆ Set.univ

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
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}
⊢ (codiscreteWithin (Ι 0 π)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin x) 2)) fun (x : ℝ) ↦
    log 4 + 2 * log (sin x)

Tactic:
apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)

Premises used: Filter.codiscreteWithin_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) Set.univ x
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
⊢ AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ

Tactic:
have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
⊢ ∀ (hx : 4 * HPow.hPow (β := ℕ) (sin (π / 2)) 2 ≠ 0),
    Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0}ᶜ ∈ codiscrete ℝ

Tactic:
have := this.preimage_zero_mem_codiscrete (x := π / 2)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this :
  ∀ (hx : 4 * HPow.hPow (β := ℕ) (sin (π / 2)) 2 ≠ 0),
    Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0}ᶜ ∈ codiscrete ℝ
⊢ (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ

Tactic:
simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this

Premises used: one_pow, Real.sin_pi_div_two, OfNat.ofNat_ne_zero, ne_eq, forall_const, Set.preimage_compl, mul_one, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this : (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ
h :
  ∀ (a : ℝ)
    (ha : Membership.mem (γ := Set ℝ) (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ a),
    log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
⊢ 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:
filter_upwards [this] with a ha
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this : (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ a
⊢ ¬sin a = 0

Tactic:
simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero,
      OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha

Premises used: OfNat.ofNat_ne_zero, pow_eq_zero_iff, false_or, mul_eq_zero, ne_eq, Set.mem_singleton_iff, not_false_eq_true, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this : (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : ¬sin a = 0
⊢ Ne (α := ℝ) 4 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this : (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : ¬sin a = 0
⊢ HPow.hPow (β := ℕ) (sin a) 2 ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
this_1 : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
this : (Set.preimage (β := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : ¬sin a = 0
h : log 4 + log (HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
h₁ : log 4 + (↑2 : ℝ) * log (sin a) = log 4 + 2 * log (sin a)
h₂ h₃ : log 4 + 2 * log (sin a) = log 4 + 2 * log (sin a)
⊢ log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)

Tactic:
rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Real.log_pow, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2 * log (sin x)) volume 0 π

Tactic:
apply intervalIntegrable_log_sin.const_mul 2

Premises used: OfNat.ofNat, intervalIntegrable_log_sin, IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π, log 4) (∫ (x : ℝ) in 0..π, 2 * log (sin x)) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
rw₁ rw₂ :
  (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x)) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
⊢ ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))

Tactic:
rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]

Premises used: intervalIntegrable_const, intervalIntegral.integral_add, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
⊢ 4 = HMul.hMul (α := ℝ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
simp : π * (log 2 + log 2) + 2 * (-log 2 * π) = 0
⊢ (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x)) = 0

Tactic:
simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi,
      (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero]

Premises used: sub_zero, two_ne_zero, integral_log_sin_zero_pi, smul_eq_mul, Real.log_mul, intervalIntegral.integral_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
⊢ π * (log 2 + log 2) + 2 * (-log 2 * π) = 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
calc :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)
    (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2))
calc₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2)) (∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x))
calc₂ :
  ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
calc₃ : (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x)) = 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0

Tactic:
calc ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2
  _ = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2) := by
    have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
    rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]
    simp
  _ = ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) := by
    apply integral_congr_codiscreteWithin
    apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)
    have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
    have := this.preimage_zero_mem_codiscrete (x := π / 2)
    simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this
    filter_upwards [this] with a ha
    simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero,
      OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha
    rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]
  _ = (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) := by
    rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]
  _ = 0 := by
    simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi,
      (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero]
    ring

Premises used: Real.pi, HMul.hMul, intervalIntegral, Real.log, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
simp : π = 0 ∨ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) 0 1) 0

Tactic:
simp only [circleAverage, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero, OfNat.ofNat_ne_zero,
    or_false]

Premises used: inv_eq_zero, OfNat.ofNat_ne_zero, mul_eq_zero, or_false, mul_inv_rev, smul_eq_mul, Real.circleAverage
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
h₁ : Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
⊢ π = 0 ∨ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
⊢ ∃ (ζ : ℝ), a⁻¹ = circleMap 0 1 ζ

Tactic:
simp [Set.exists_range_iff.1, h]

Premises used: Set.exists_range_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
Goal:
a : ℂ
h : ‖a‖ = 1
h₁ : ∀ (ζ : ℝ) (hζ : a⁻¹ = circleMap 0 1 ζ), Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0

Tactic:
obtain ⟨ζ, hζ⟩ : ∃ ζ, a⁻¹ = circleMap 0 1 ζ := by simp [Set.exists_range_iff.1, h]