awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
pos :
  ∀ (i : ℝ),
    IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) i) : ℝ) * log ‖x - i‖) volume a b
⊢ IntervalIntegrable (ε := ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
    volume a b

Tactic:
apply IntervalIntegrable.finsum

Premises used: IntervalIntegrable.finsum
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) i) : ℝ) * log ‖x - i‖) volume a b

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
⊢ a = a - i + i

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
⊢ b = b - i + i

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume (a - i + i) (b - i + i)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume a b

Tactic:
rw [(by ring : a = ((a - i) + i)), (by ring : b = ((b - i) + i))]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x‖) volume (a - i) (b - i)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x - i‖) volume (a - i + i) (b - i + i)

Tactic:
apply IntervalIntegrable.comp_sub_right (f := (log ‖·‖)) _ i

Premises used: IntervalIntegrable.comp_sub_right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
i : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖x‖) volume (a - i) (b - i)

Tactic:
simp [norm_eq_abs, log_abs]

Premises used: Real.log_abs, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
pos : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) volume a b

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
pos : ∀ x ∈ [[a, b]], ‖g x‖ ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ log ‖g x‖) [[a, b]]

Tactic:
apply h₁g.continuousOn.norm.log

Premises used: ContinuousOn.log, AnalyticOnNhd.continuousOn, ContinuousOn.norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : (↑[[a, b]] : Type)), g (↑u : ℝ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin [[a, b]]]
    HSMul.hSMul (α := ℝ → ℝ)
      (∏ᶠ (u : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℤ) (fun (x : ℝ) ↦ x - u) ((divisor f [[a, b]] : (a : ℝ) → ℤ) u : ℤ)) g
h₄g :
  (fun (x : ℝ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    HAdd.hAdd (α := ℝ → ℝ) (∑ᶠ (u : ℝ), fun (x : ℝ) ↦ (↑((divisor f [[a, b]] : (a : ℝ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℝ) ↦ log ‖g x‖
⊢ ∀ x ∈ [[a, b]], ‖g x‖ ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ¬∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
⊢ ¬∃ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤

Tactic:
rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_Icc inf_le_sup)] at t₀

Premises used: isConnected_Icc, inf_le_sup, MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ¬∃ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) ≠ ⊤
⊢ ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤

Tactic:
push Not at t₀

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
apply : (codiscreteWithin [[a, b]]).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
⊢ (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0

Tactic:
apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)

Premises used: Filter.codiscreteWithin_mono, Filter.EventuallyEq.filter_mono, Set.uIoc_subset_uIcc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
h : ∀ (x : ℝ) (h₁x : MeromorphicNFAt f x) (h₂x : x ∈ [[a, b]]), log ‖f x‖ = 0 x
⊢ (codiscreteWithin [[a, b]]).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0

Tactic:
filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x

Premises used: MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin, Filter.self_mem_codiscreteWithin, Set.uIcc
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
h : f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
⊢ log ‖f x‖ = 0 x

Tactic:
simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, Pi.zero_apply, Real.log_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
h : f x = 0
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
h : ∀ (hCon : ¬f x = 0), False
⊢ f x = 0

Tactic:
by_contra hCon
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
hCon : ¬f x = 0
⊢ False

Tactic:
simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]

Premises used: Subtype.mk, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
⊢ (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0

Tactic:
have : (log ‖f ·‖) =ᶠ[Filter.codiscreteWithin (Ι a b)] 0 := by
      apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)
      filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x
      simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
      left
      by_contra hCon
      simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
neg : IntervalIntegrable (ε := ℝ) 0 volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b

Tactic:
rw [intervalIntegrable_congr_codiscreteWithin this]

Premises used: intervalIntegrable_congr_codiscreteWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
neg : Real.zero✝ = 0 ∨ LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
⊢ IntervalIntegrable (ε := ℝ) 0 volume a b

Tactic:
apply Iff.mpr _root_.intervalIntegrable_const_iff

Premises used: Iff.mpr, intervalIntegrable_const_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : (↑[[a, b]] : Type)), meromorphicOrderAt f (↑u : ℝ) = ⊤
this : (codiscreteWithin (Ι a b)).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) 0
neg neg₁ : ¬Real.zero✝ = 0 → LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)
⊢ Real.zero✝ = 0 ∨ LT.lt (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ι a b) : ENNReal) (⊤ : ENNReal)

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
simp_rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log⁺ ‖f x‖) volume a b

Tactic:
simp_rw [← half_mul_log_add_log_abs, mul_add]

Premises used: mul_add, Real.half_mul_log_add_log_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖) volume a b
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * |log ‖f x‖|) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b

Tactic:
apply IntervalIntegrable.add

Premises used: IntervalIntegrable.add
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * log ‖f x‖) volume a b

Tactic:
apply hf.intervalIntegrable_log_norm.const_mul

Premises used: MeromorphicOn.intervalIntegrable_log_norm, IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2⁻¹ * |log ‖f x‖|) volume a b

Tactic:
apply hf.intervalIntegrable_log_norm.abs.const_mul

Premises used: MeromorphicOn.intervalIntegrable_log_norm, IntervalIntegrable.abs, IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
a b : ℝ
f : ℝ → ℝ
hf : MeromorphicOn f [[a, b]]
⊢ log ∘ f = fun (x : ℝ) ↦ log ‖f x‖

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
a b : ℝ
f : ℝ → ℝ
hf : MeromorphicOn f [[a, b]]
rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b
⊢ IntervalIntegrable (log ∘ f) volume a b

Tactic:
rw [(by aesop : log ∘ f = (log ‖f ·‖))]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
a b : ℝ
f : ℝ → ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖f x‖) volume a b

Tactic:
exact hf.intervalIntegrable_log_norm

Premises used: MeromorphicOn.intervalIntegrable_log_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
a b : ℝ
⊢ IntervalIntegrable (log ∘ sin) volume a b

Tactic:
analyticOnNhd_sin.meromorphicOn.intervalIntegrable_log

Premises used: Real.analyticOnNhd_sin, MeromorphicOn.intervalIntegrable_log, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
a b : ℝ
⊢ IntervalIntegrable (log ∘ cos) volume a b

Tactic:
analyticOnNhd_cos.meromorphicOn.intervalIntegrable_log

Premises used: Real.analyticOnNhd_cos, MeromorphicOn.intervalIntegrable_log, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
pos :
  ∀ (t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
neg :
  ∀ (t₀ : ¬∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R

Tactic:
by_cases t₀ : ∀ u : (sphere c |R|), meromorphicOrderAt f u ≠ ⊤
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
pos :
  ∀ (g : ℂ → E) (h₁g : AnalyticOnNhd ℂ g (sphere c |R|)) (h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0)
    (h₃g :
      f =ᶠ[codiscreteWithin (sphere c |R|)]
        HSMul.hSMul (α := ℂ → ℂ)
          (∏ᶠ (u : ℂ),
            HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
          g),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((divisor f (sphere c |R|)).finiteSupport (isCompact_sphere c |R|))

Premises used: abs, Function.locallyFinsuppWithin.finiteSupport, MeromorphicOn.divisor, isCompact_sphere, MeromorphicOn.extract_zeros_poles, Metric.sphere
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
⊢ (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖

Tactic:
have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
pos :
  CircleIntegrable
    (HAdd.hAdd (α := ℂ → ℝ)
      (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : ℂ) ↦
      log ‖g x‖)
    c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R

Tactic:
apply CircleIntegrable.congr_codiscreteWithin h₄g.symm

Premises used: CircleIntegrable.congr_codiscreteWithin, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
pos :
  CircleIntegrable (E := ℝ)
    (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R
pos₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖g x‖) c R
⊢ CircleIntegrable
    (HAdd.hAdd (α := ℂ → ℝ)
      (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : ℂ) ↦
      log ‖g x‖)
    c R

Tactic:
apply CircleIntegrable.add

Premises used: CircleIntegrable.add