awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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
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)
⊢ 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:
nth_rw 2 [← circleAverage_const (log s.card) 0 r]

Premises used: Nat.cast, Real.log, Finset.card, OfNat.ofNat, Real.circleAverage_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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
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
⊢ 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:
rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]

Premises used: Real.circleAverage_sum, Nat.cast, Real.log, CircleIntegrable.sum, Finset.card, Real.circleAverage_add, OfNat.ofNat, circleIntegrable_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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
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 : ℝ)
⊢ 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:
congr 1
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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
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
⊢ (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:
ext x
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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 : ℂ
⊢ ∑ 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:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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)
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 : ℝ)
⊢ 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:
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

Premises used: Norm.norm, Real.posLog, Nat.cast, Real.log, HAdd.hAdd, Finset.card, OfNat.ofNat, Finset.sum, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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)))
1 :
  Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) →
    Meromorphic (![f₁, f₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)))
⊢ Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ i → Meromorphic (![f₁, f₂] i)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ 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)))

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) →
    Meromorphic (![f₁, f₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)))

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ + f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤ + fun (x : ℝ) ↦ log 2

Tactic:
simpa using proximity_sum_top_le Finset.univ ![f₁, f₂]
    (fun i ↦ by fin_cases i <;> aesop)

Premises used: Finset.univ, ValueDistribution.proximity_sum_top_le, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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
h : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 |r|) x → log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
⊢ 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)

Tactic:
apply circleAverage_mono

Premises used: Real.circleAverage_mono
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x * f₂ x‖) 0 r
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r

Tactic:
simp_rw [← norm_mul]

Premises used: norm_mul
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hf₁ : MeromorphicOn (E := ℂ) (fun (x : ℂ) ↦ f₁ x * f₂ x) (sphere 0 |r|)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x * f₂ x‖) 0 r

Tactic:
apply MeromorphicOn.circleIntegrable_posLog_norm

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hf₁ : Meromorphic (E := ℂ) fun (x : ℂ) ↦ f₁ x * f₂ x
⊢ MeromorphicOn (E := ℂ) (fun (x : ℂ) ↦ f₁ x * f₂ x) (sphere 0 |r|)

Tactic:
apply Meromorphic.meromorphicOn

Premises used: Meromorphic.meromorphicOn
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ Meromorphic (E := ℂ) fun (x : ℂ) ↦ f₁ x * f₂ x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

Tactic:
apply (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)).add
          (MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x))

Premises used: MeromorphicOn.circleIntegrable_posLog_norm, CircleIntegrable.add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 |r|) x → log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
fun _ _ ↦ posLog_mul

Premises used: Real.posLog_mul
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 |r|) x → log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
exact fun _ _ ↦ posLog_mul

Premises used: Real.posLog_mul
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
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
⊢ 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:
ext r
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
h : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0 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

Tactic:
apply circleAverage_add

Premises used: Real.circleAverage_add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0 r

Tactic:
MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0 r

Tactic:
exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0 r

Tactic:
MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0 r

Tactic:
exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) =
    proximity f₁ ⊤ + proximity f₂ ⊤

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
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)
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)
calc₃ :
  HAdd.hAdd (α := (R : ℝ) → ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₁ x‖) 0)
      (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f₂ x‖) 0) =
    proximity f₁ ⊤ + proximity f₂ ⊤
⊢ proximity (f₁ * f₂) ⊤ ≤ proximity f₁ ⊤ + proximity f₂ ⊤

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]

Premises used: Norm.norm, HMul.hMul, Real.posLog, HAdd.hAdd, ValueDistribution.proximity, Top.top, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
rw : proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
rw [← proximity_inv, mul_inv]

Premises used: mul_inv, ValueDistribution.proximity_inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv

Premises used: ValueDistribution.proximity_mul_top_le, Meromorphic.inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
rw : proximity f₁ 0 + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
rw₁ rw₂ : proximity f₁ 0 + proximity f₂ 0 = proximity f₁ 0 + proximity f₂ 0
⊢ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0

Tactic:
rw [proximity_inv, proximity_inv]

Premises used: ValueDistribution.proximity_inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
calc : proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
calc₁ : proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤ = proximity f₁ 0 + proximity f₂ 0
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0

Tactic:
calc proximity (f₁ * f₂) 0
    _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv
    _ = (proximity f₁ 0) + (proximity f₂ 0) := by
      rw [proximity_inv, proximity_inv]

Premises used: HMul.hMul, Inv.inv, ValueDistribution.proximity, Top.top, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
n : ℕ
h : ∀ (x : ℝ), proximity (f ^ n) ⊤ x = (n • proximity f ⊤) x
⊢ proximity (f ^ n) ⊤ = n • proximity f ⊤

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
n : ℕ
x : ℝ
⊢ proximity (f ^ n) ⊤ x = (n • proximity f ⊤) x

Tactic:
simp [proximity, ← smul_eq_mul, circleAverage_fun_smul]

Premises used: Real.circleAverage_fun_smul, smul_eq_mul, ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
n : ℕ
rw : proximity (f ^ n)⁻¹ ⊤ = n • proximity f 0
rw₁ : proximity (f ^ n)⁻¹ ⊤ = n • proximity f⁻¹ ⊤
rw₂ : proximity (f⁻¹ ^ n) ⊤ = n • proximity f⁻¹ ⊤
rw₃ rw₄ : n • proximity f⁻¹ ⊤ = n • proximity f⁻¹ ⊤
⊢ proximity (f ^ n) 0 = n • proximity f 0

Tactic:
rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]

Premises used: ValueDistribution.proximity_inv, inv_pow, ValueDistribution.proximity_pow_top
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x y : ℝ
hx : x ∈ s
hy : y ∈ s
⊢ BoundedVariationOn f (s ∩ Icc x y)

Tactic:
simp only [BoundedVariationOn, h hx hy, Ne, ENNReal.ofReal_ne_top, not_false_iff]

Premises used: Ne, ENNReal.ofReal_ne_top, not_false_iff, BoundedVariationOn
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
refl : ∀ (hy : x ∈ s), eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal ((↑l : ℝ) * (x - x))
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
cases hs hx hy
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
refl : 0 = ENNReal.ofReal ((↑l : ℝ) * (x - x))
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal ((↑l : ℝ) * (x - x))

Tactic:
rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]

Premises used: And.left, eVariationOn.subsingleton
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal ((↑l : ℝ) * (x - x))

Tactic:
simp only [sub_self, mul_zero, ENNReal.ofReal_zero]

Premises used: sub_self, MulZeroClass.mul_zero, ENNReal.ofReal_zero
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
refine :
  ∀
    (h :
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
    (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
refine ⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
inl : ∀ (xy : x ≤ y), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
inr : ∀ (yx : y ≤ x), eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
rcases le_total x y with (xy | yx)

Premises used: le_total
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
h xs ys xy
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
exact h xs ys xy
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
inr : (↑l : ℝ) * (y - x) ≤ 0
inr₁ : (s ∩ Icc x y).Subsingleton
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
rw [eVariationOn.subsingleton, ENNReal.ofReal_of_nonpos]

Premises used: ENNReal.ofReal_of_nonpos, eVariationOn.subsingleton
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ (↑l : ℝ) * (y - x) ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos l.prop (sub_nonpos_of_le yx)

Premises used: Subtype.prop, sub_nonpos_of_le, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ (↑l : ℝ) * (y - x) ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos l.prop (sub_nonpos_of_le yx)

Premises used: Subtype.prop, sub_nonpos_of_le, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
z : ℝ
zs : z ∈ s
xz : x ≤ z
zy : z ≤ y
w : ℝ
ws : w ∈ s
xw : x ≤ w
wy : w ≤ y
inr : ∀ (zs : x ∈ s) (xz : x ≤ x) (zy : x ≤ y), x = w
⊢ z = w

Tactic:
cases le_antisymm (zy.trans yx) xz

Premises used: le_antisymm, LE.le.trans
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
w : ℝ
ws : w ∈ s
xw : x ≤ w
wy : w ≤ y
zs : x ∈ s
xz : x ≤ x
zy : x ≤ y
inr : ∀ (ws : x ∈ s) (xw : x ≤ x) (wy : x ≤ y), x = x
⊢ x = w

Tactic:
cases le_antisymm (wy.trans yx) xw

Premises used: le_antisymm, LE.le.trans