awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
right : ‖r‖ = r
right₁ right₂ : r = r
⊢ ‖r‖ / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ = r

Tactic:
rw [div_mul_cancel₀ _ (by simpa using τ.ne_zero), Real.norm_of_nonneg hr']

Premises used: div_mul_cancel₀, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
simp_rw : log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a + f x) 0)) = 0
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = 0

Tactic:
simp_rw [sub_eq_neg_add]

Premises used: sub_eq_neg_add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
rw : log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a) 0)) = 0
rw₁ : meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ -a) 0 < meromorphicOrderAt f 0
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a + f x) 0)) = 0

Tactic:
rw [(meromorphicAt_of_meromorphicOrderAt_ne_zero
    h.ne').meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt]

Premises used: LT.lt.ne', meromorphicAt_of_meromorphicOrderAt_ne_zero, MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a) 0)) = 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
rw : (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0
⊢ meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ -a) 0 < meromorphicOrderAt f 0

Tactic:
rw [meromorphicOrderAt_const]

Premises used: meromorphicOrderAt_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
h :
  ∀ (a : ℂ) (ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a)
    (ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a),
    log ‖meromorphicTrailingCoeffAt f 0 - a‖ =
      log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖)
    fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))

Tactic:
filter_upwards [self_mem_codiscreteWithin (sphere 0 |1|), compl_singleton_mem_codiscreteWithin
    (meromorphicTrailingCoeffAt f 0)] with a ha_sphere ha_ne

Premises used: abs, compl_singleton_mem_codiscreteWithin, Filter.self_mem_codiscreteWithin, meromorphicTrailingCoeffAt, OfNat.ofNat, Metric.sphere
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
h : meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0
⊢ log ‖meromorphicTrailingCoeffAt f 0 - a‖ =
    log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
h : meromorphicOrderAt f 0 = meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
h₃ : meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ a) 0 ≠ 0
⊢ meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0

Tactic:
rw [h₁.meromorphicTrailingCoeffAt_fun_sub_eq_sub
    (by fun_prop), meromorphicTrailingCoeffAt_const, sub_eq_add_neg]

Premises used: sub_eq_add_neg, meromorphicTrailingCoeffAt_const, MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_sub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
h : meromorphicOrderAt f 0 = if a = 0 then ⊤ else 0
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
simp only [meromorphicOrderAt_const]

Premises used: meromorphicOrderAt_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ meromorphicOrderAt f 0 = if a = 0 then ⊤ else 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
h : ¬meromorphicTrailingCoeffAt f 0 - a = 0
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ a) 0 ≠ 0

Tactic:
simp only [meromorphicTrailingCoeffAt_const, ne_eq]

Premises used: meromorphicTrailingCoeffAt_const, ne_eq
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ ¬meromorphicTrailingCoeffAt f 0 - a = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
pos :
  ∀ (h : ¬MeromorphicAt f 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
neg :
  ∀ (h : ¬¬MeromorphicAt f 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
by_cases h: ¬MeromorphicAt f 0

Premises used: OfNat.ofNat, MeromorphicAt
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
rwa rwa₁ rwa₂ rwa₃ : ¬MeromorphicAt f 0
⊢ ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0

Tactic:
rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]

Premises used: MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
⊢ ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0

Tactic:
have {a : ℂ} : ¬MeromorphicAt (fun x ↦ f x - a) 0 := by
      rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
this : ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
neg :
  ∀ (hneg : meromorphicOrderAt f 0 < 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
neg₁ :
  ∀ (hzero : meromorphicOrderAt f 0 = 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
neg₂ :
  ∀ (hpos : 0 < meromorphicOrderAt f 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos

Premises used: meromorphicOrderAt, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
(circleIntegrable_congr fun a ha ↦ ?_).2 (circleIntegrable_const
      (log ‖meromorphicTrailingCoeffAt f 0‖) 0 1)

Premises used: Iff.mpr, Norm.norm, Real.log, meromorphicTrailingCoeffAt, OfNat.ofNat, circleIntegrable_const, circleIntegrable_congr
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
neg : meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]

Premises used: MeromorphicAt.const, MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
neg : meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
rw [meromorphicOrderAt_const]

Premises used: meromorphicOrderAt_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
neg : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
apply CircleIntegrable.congr_codiscreteWithin
     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)

Premises used: _private.0.ValueDistribution.eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero, Classical.not_not, Iff.mp, CircleIntegrable.congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1

Tactic:
simpa [norm_sub_rev] using circleIntegrable_log_norm_sub_const 1

Premises used: norm_sub_rev, circleIntegrable_log_norm_sub_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hpos : 0 < meromorphicOrderAt f 0
apply :
  EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
    (fun (x : ℂ) ↦ 0) (sphere 0 |1|)
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1

Tactic:
apply (circleIntegrable_congr _).2 (circleIntegrable_const 0 0 1)

Premises used: Iff.mpr, OfNat.ofNat, circleIntegrable_const, circleIntegrable_congr
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hpos : 0 < meromorphicOrderAt f 0
⊢ EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
    (fun (x : ℂ) ↦ 0) (sphere 0 |1|)

Tactic:
fun _ ↦ log_trailingCoeff_eq_zero_on_unitSphere hpos

Premises used: _private.0.ValueDistribution.log_trailingCoeff_eq_zero_on_unitSphere, Set.EqOn
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hpos : 0 < meromorphicOrderAt f 0
⊢ EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
    (fun (x : ℂ) ↦ 0) (sphere 0 |1|)

Tactic:
exact fun _ ↦ log_trailingCoeff_eq_zero_on_unitSphere hpos

Premises used: _private.0.ValueDistribution.log_trailingCoeff_eq_zero_on_unitSphere
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : 0 < meromorphicOrderAt f 0
⊢ Eq (α := ℝ)
    (circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1)
    0

Tactic:
circleAverage_const_on_circle (fun _ hx ↦ log_trailingCoeff_eq_zero_on_unitSphere h hx)

Premises used: _private.0.ValueDistribution.log_trailingCoeff_eq_zero_on_unitSphere, Real.circleAverage_const_on_circle
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
pos :
  ∀ (hf : MeromorphicAt f 0),
    circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
      log⁺ ‖meromorphicTrailingCoeffAt f 0‖
neg :
  ∀ (hf : ¬MeromorphicAt f 0),
    circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
      log⁺ ‖meromorphicTrailingCoeffAt f 0‖
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
by_cases hf : MeromorphicAt f 0

Premises used: OfNat.ofNat, MeromorphicAt
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
pos : circleAverage (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]

Premises used: _private.0.ValueDistribution.eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero, zero_ne_one, Ne.symm, Real.circleAverage_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
pos : circleAverage (fun (x : ℂ) ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp_rw [norm_sub_rev]

Premises used: norm_sub_rev
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
pos pos₁ : log⁺ ‖meromorphicTrailingCoeffAt f 0‖ = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [circleAverage_log_norm_sub_const_eq_posLog]

Premises used: circleAverage_log_norm_sub_const_eq_posLog
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
a : ℂ
⊢ MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
a : ℂ
rwa rwa₁ rwa₂ rwa₃ : ¬MeromorphicAt f 0
⊢ ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0

Tactic:
rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]

Premises used: MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
⊢ ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0

Tactic:
have {a : ℂ} : ¬ MeromorphicAt (fun x ↦ f x - a) 0 := by
    rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
this : ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp_all [circleAverage_const]

Premises used: Real.circleAverage_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
rw :
  EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
    (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0‖) (sphere 0 |1|)
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [circleAverage_congr_sphere (f₂ := fun _ ↦ log ‖meromorphicTrailingCoeffAt f 0‖),
    circleAverage_const]

Premises used: Real.circleAverage_congr_sphere, Real.circleAverage_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
e_x : meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0 = meromorphicTrailingCoeffAt f 0
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
congr 2
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
e_x : meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
⊢ meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0 = meromorphicTrailingCoeffAt f 0

Tactic:
rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]

Premises used: MeromorphicAt.const, MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
e_x : meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0

Tactic:
rw [meromorphicOrderAt_const]

Premises used: meromorphicOrderAt_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
⊢ characteristic f a r = characteristic g a r

Tactic:
simp [characteristic, proximity_congr_codiscrete hfg hr, logCounting_congr_codiscrete hfg]

Premises used: ValueDistribution.characteristic, ValueDistribution.logCounting_congr_codiscrete, ValueDistribution.proximity_congr_codiscrete
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
h : Meromorphic f
a₀ : E
⊢ characteristic f ⊤ - characteristic.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤ =
    proximity f ⊤ - proximity.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤

Tactic:
simp [← Pi.sub_def, characteristic, logCounting_sub_const h]

Premises used: ValueDistribution.logCounting_sub_const, ValueDistribution.characteristic, Pi.sub_def
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
⊢ Function.Even (characteristic f a)

Tactic:
proximity_even.add logCounting_even

Premises used: ValueDistribution.characteristic, Function.Even.add, ValueDistribution.proximity_even, ValueDistribution.logCounting_even
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
r : ℝ
hr : 1 ≤ r
⊢ 0 ≤ characteristic f a r

Tactic:
add_nonneg (proximity_nonneg r) (logCounting_nonneg hr)

Premises used: ValueDistribution.proximity_nonneg, ValueDistribution.logCounting_nonneg, ValueDistribution.characteristic, add_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
x : ℝ
hr : 1 ≤ x
⊢ 0 x ≤ characteristic f a x

Tactic:
simp [characteristic_nonneg hr]

Premises used: ValueDistribution.characteristic_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ characteristic f a x) x} x}
      a_1
h₁ : ∀ (a_1 : ℝ), 1 ≤ a_1 → 0 a_1 ≤ characteristic f a a_1
⊢ 0 ≤ᶠ[atTop] characteristic f a

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1] using fun _ hr ↦ by simp [characteristic_nonneg hr]

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
simp :
  proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
⊢ characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, characteristic (f a) ⊤) r + log (↑s.card : ℝ)

Tactic:
simp only [characteristic, Pi.add_apply, Finset.sum_apply]

Premises used: Finset.sum_apply, ValueDistribution.characteristic, Pi.add_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
h₁ : proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ)
h₂ : logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
gcongr