awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h :
  circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
⊢ HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
have h₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R
Tactic: rw [← circleAverage_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h :
  circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
h₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R
⊢ HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
have h₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R
Tactic: rw [← circleAverage_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
have h : circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
  circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖ - log⁺ ‖f x‖⁻¹) 0 R
Tactic: simp_rw [← posLog_sub_posLog_inv, Pi.sub_def]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R
have h : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖(f x)⁻¹‖) 0 R
Tactic: simp_rw [← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
⊢ proximity f a (-r) = proximity f a r
have pos : ∀ (h : a = ⊤), proximity f a (-r) = proximity f a r
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
pos : ∀ (h : a = ⊤), proximity f a (-r) = proximity f a r
⊢ proximity f a (-r) = proximity f a r
have neg : ∀ (h : ¬a = ⊤), proximity f a (-r) = proximity f a r
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
⊢ 0 ≤ proximity f a
have pos : ∀ (h : a = ⊤), 0 ≤ proximity f a
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
pos : ∀ (h : a = ⊤), 0 ≤ proximity f a
⊢ 0 ≤ proximity f a
have neg : ∀ (h : ¬a = ⊤), 0 ≤ proximity f a
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ ≤
    HAdd.hAdd (α := ℝ → ℝ) (∑ a ∈ s, proximity (f a) ⊤) fun (x : ℝ) ↦ log (↑s.card : ℝ)
have simp : circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 ≤
  HAdd.hAdd (α := ℝ → ℝ) (∑ x ∈ s, circleAverage (fun (x_1 : ℂ) ↦ log⁺ ‖f x x_1‖) 0) fun (x : ℝ) ↦ log (↑s.card : ℝ)
Tactic: simp only [proximity_top, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ x ∈ s, circleAverage (fun (x_1 : ℂ) ↦ log⁺ ‖f x x_1‖) 0)
      (fun (x : ℝ) ↦ log (↑s.card : ℝ)) r
have h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
Tactic: have h₂f : ∀ i ∈ s, CircleIntegrable (log⁺ ‖f i ·‖) 0 r :=
    fun i hi ↦ MeromorphicOn.circleIntegrable_posLog_norm (fun x hx ↦ hf i hi x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ x ∈ s, circleAverage (fun (x_1 : ℂ) ↦ log⁺ ‖f x x_1‖) 0)
      (fun (x : ℝ) ↦ log (↑s.card : ℝ)) r
have simp : circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
  ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
Tactic: simp only [Pi.add_apply, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
    (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)
have hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r
⊢ LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
    (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)
have hf₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r
hf₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r
⊢ LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
    (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)
have h : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) (sphere 0 |r|) x →
    log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : Membership.mem (γ := Set ℂ) (sphere 0 |r|) x
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)
have h : log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ log (↑s.card : ℝ) + ∑ c ∈ s, log⁺ ‖f c x‖
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
    ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
have nth_rw : circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
  HAdd.hAdd (α := ℝ) (∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log (↑s.card : ℝ)) 0 r)
Tactic: nth_rw 2 [← circleAverage_const (log s.card) 0 r]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
    HAdd.hAdd (α := ℝ) (∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r)
      (circleAverage (fun (x : ℂ) ↦ log (↑s.card : ℝ)) 0 r)
have rw : circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
  circleAverage (HAdd.hAdd (α := ℂ → ℝ) (∑ i ∈ s, fun (x : ℂ) ↦ log⁺ ‖f i x‖) fun (x : ℂ) ↦ log (↑s.card : ℝ)) 0 r
Tactic: rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
    circleAverage (HAdd.hAdd (α := ℂ → ℝ) (∑ i ∈ s, fun (x : ℂ) ↦ log⁺ ‖f i x‖) fun (x : ℂ) ↦ log (↑s.card : ℝ)) 0 r
have e_f : (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) =
  HAdd.hAdd (α := ℂ → ℝ) (∑ i ∈ s, fun (x : ℂ) ↦ log⁺ ‖f i x‖) fun (x : ℂ) ↦ log (↑s.card : ℝ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) =
    HAdd.hAdd (α := ℂ → ℝ) (∑ i ∈ s, fun (x : ℂ) ↦ log⁺ ‖f i x‖) fun (x : ℂ) ↦ log (↑s.card : ℝ)
have e_f : ∀ (x : ℂ),
  ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ) =
    HAdd.hAdd (α := ℂ → ℝ) (β := ℂ → ℝ) (∑ i ∈ s, fun (x : ℂ) ↦ log⁺ ‖f i x‖) (fun (x : ℂ) ↦ log (↑s.card : ℝ)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
have calc : LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
  (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)
Tactic: calc circleAverage (log⁺ ‖∑ c ∈ s, f c ·‖) 0 r
    _ ≤ circleAverage (∑ c ∈ s, log⁺ ‖f c ·‖ + log s.card) 0 r := by
      apply circleAverage_mono
      · apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm
      · apply (CircleIntegrable.fun_sum s h₂f).add (circleIntegrable_const _ _ _)
      · intro x hx
        rw [add_comm]
        apply posLog_norm_sum_le
    _ = ∑ c ∈ s, circleAverage (log⁺ ‖f c ·‖) 0 r + log s.card := by
      nth_rw 2 [← circleAverage_const (log s.card) 0 r]
      rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]
      congr 1
      ext x
      simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
calc :
  LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
    (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
have calc₁ : circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r =
  ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
Tactic: calc circleAverage (log⁺ ‖∑ c ∈ s, f c ·‖) 0 r
    _ ≤ circleAverage (∑ c ∈ s, log⁺ ‖f c ·‖ + log s.card) 0 r := by
      apply circleAverage_mono
      · apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm
      · apply (CircleIntegrable.fun_sum s h₂f).add (circleIntegrable_const _ _ _)
      · intro x hx
        rw [add_comm]
        apply posLog_norm_sum_le
    _ = ∑ c ∈ s, circleAverage (log⁺ ‖f c ·‖) 0 r + log s.card := by
      nth_rw 2 [← circleAverage_const (log s.card) 0 r]
      rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]
      congr 1
      ext x
      simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
i : Fin (Nat.succ 0).succ
⊢ Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ i → Meromorphic (![f₁, f₂] i)
have 0 : Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) →
  Meromorphic (![f₁, f₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
i : Fin (Nat.succ 0).succ
0 :
  Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) →
    Meromorphic (![f₁, f₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)))
⊢ Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ i → Meromorphic (![f₁, f₂] i)
have 1 : Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) →
  Meromorphic (![f₁, f₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ LE.le (α := (fun (R : ℝ) ↦ ℝ) r) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r)
have hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r
⊢ LE.le (α := (fun (R : ℝ) ↦ ℝ) r) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r)
have hf₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r
hf₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r
⊢ LE.le (α := (fun (R : ℝ) ↦ ℝ) r) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r)
have h : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 |r|) x → log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
Tactic: apply circleAverage_mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r
have hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x * f₂ x‖) 0 r
Tactic: simp_rw [← norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x * f₂ x‖) 0 r
have hf₁ : MeromorphicOn (E := ℂ) (fun (x : ℂ) ↦ f₁ x * f₂ x) (sphere 0 |r|)
Tactic: apply MeromorphicOn.circleIntegrable_posLog_norm
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ MeromorphicOn (E := ℂ) (fun (x : ℂ) ↦ f₁ x * f₂ x) (sphere 0 |r|)
have hf₁ : Meromorphic (E := ℂ) fun (x : ℂ) ↦ f₁ x * f₂ x
Tactic: apply Meromorphic.meromorphicOn
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 =
    HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0)
have h : ∀ (r : ℝ),
  circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r =
    HAdd.hAdd (α := (R : ℝ) → ℝ) (β := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) r
Tactic: ext r
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r =
    HAdd.hAdd (α := (R : ℝ) → ℝ) (β := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) r
have h : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0 r
Tactic: apply circleAverage_add
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
h : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0 r
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r =
    HAdd.hAdd (α := (R : ℝ) → ℝ) (β := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) r
have h₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0 r
Tactic: apply circleAverage_add
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤
have calc : proximity (f₁ * f₂) ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0
Tactic: calc proximity (f₁ * f₂) ⊤
    _ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
      simp [proximity]
    _ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
      intro r
      apply circleAverage_mono
      · simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop
      · apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))
      · exact fun _ _ ↦ posLog_mul
    _ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0 := by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)
    _ = proximity f₁ ⊤ + proximity f₂ ⊤ := by simp [proximity]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
calc : proximity (f₁ * f₂) ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤
have calc₁ : LE.le (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0)
  (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0)
Tactic: calc proximity (f₁ * f₂) ⊤
    _ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
      simp [proximity]
    _ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
      intro r
      apply circleAverage_mono
      · simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop
      · apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))
      · exact fun _ _ ↦ posLog_mul
    _ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0 := by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)
    _ = proximity f₁ ⊤ + proximity f₂ ⊤ := by simp [proximity]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
calc : proximity (f₁ * f₂) ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0
calc₁ :
  LE.le (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0)
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤
have calc₂ : circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 =
  HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0)
Tactic: calc proximity (f₁ * f₂) ⊤
    _ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 := by
      simp [proximity]
    _ ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 := by
      intro r
      apply circleAverage_mono
      · simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop
      · apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))
      · exact fun _ _ ↦ posLog_mul
    _ = circleAverage (log⁺ ‖f₁ ·‖) 0 + circleAverage (log⁺ ‖f₂ ·‖) 0 := by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)
    _ = proximity f₁ ⊤ + proximity f₂ ⊤ := by simp [proximity]