awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
⊢ 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}
have this : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
Tactic: have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
this : AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ 4 * HPow.hPow (β := ℕ) (sin x) 2) Set.univ
⊢ 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}
have this₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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 ℝ
⊢ 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}
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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 ℝ
⊢ 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}
have 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)
Tactic: filter_upwards [this] with a ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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
⊢ log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
have ha₁ : ¬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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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
⊢ log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
have h : log 4 + log (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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)
⊢ log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
have h₁ : log 4 + (↑2 : ℝ) * log (sin a) = log 4 + 2 * log (sin a)
Tactic: rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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)
⊢ log (4 * HPow.hPow (β := ℕ) (sin a) 2) = log 4 + 2 * log (sin a)
have h₂ : log 4 + 2 * log (sin a) = log 4 + 2 * log (sin a)
Tactic: rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
have 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))
Tactic: rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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))
⊢ ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) =
    (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
have 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))
Tactic: rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x)) = 0
have simp : π * (log 2 + log 2) + 2 * (-log 2 * π) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0
have calc₁ : Eq (α := ℝ) (∫ (x : ℝ) in 0..π, log (4 * HPow.hPow (β := ℕ) (sin x) 2)) (∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0
have calc₂ : ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) =
  (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
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))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) 0
have calc₃ : (∫ (x : ℝ) in 0..π, log 4) + HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π, log (sin x)) = 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
-- 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 simp : π = 0 ∨ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
Tactic: simp only [circleAverage, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero, OfNat.ofNat_ne_zero,
    or_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ = 1
⊢ π = 0 ∨ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have h₁ : Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ = 1
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖circleMap 0 1 θ - a‖) 0
have h₁ : ∀ (ζ : ℝ) (hζ : a⁻¹ = circleMap 0 1 ζ), 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
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..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
have this₁ : 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 := ζ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖)
    (∫ (x : ℝ) in 0..2 * π, log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2)
have h₁ : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ log ‖circleMap 0 1 x - 1‖)
  (fun (x : ℝ) ↦ log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2) [[0, 2 * π]]
Tactic: apply integral_congr
-- 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 * π]]
⊢ log ‖circleMap 0 1 x - 1‖ = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2
have h₁ : log ((Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1)) / 2 = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2
Tactic: rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg]
-- 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 * π]]
⊢ log ((Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1)) / 2 = log (4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2) / 2
have h₁ : (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
Tactic: congr
-- 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 * π]]
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x = 2 - 2 * cos x
have rw : HAdd.hAdd (α := ℝ) 1 1 - 2 * cos x = 2 - 2 * cos x
Tactic: rw [sin_sq_add_cos_sq]
-- 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 * π]]
⊢ 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 2))
have rw : 2 - 2 * cos x = 2 - 2 * cos (2 * x / 2)
Tactic: rw [← mul_div_assoc]
-- 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 * π]]
⊢ 2 - 2 * cos (2 * (x / 2)) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2
have rw : 2 - 2 * (2 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 - 1) = 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2
Tactic: rw [cos_two_mul]
-- 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 * π]]
⊢ 4 - 4 * HPow.hPow (β := ℕ) (cos (x / 2)) 2 = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have 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
Tactic: nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
-- 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 * π]]
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have calc : (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = (cos x - 1) * (cos x - 1) + sin x * sin x
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
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have 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
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
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have calc₂ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 + 1 - 2 * cos x = 2 - 2 * cos x
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
⊢ (Complex.normSq : (a : ℂ) → ℝ) (circleMap 0 1 x - 1) = 4 * HPow.hPow (β := ℕ) (sin (x / 2)) 2
have calc₃ : 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 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