mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s

pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)

Tactic:
·

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
·

Goal state after:
case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)

Tactic:
·

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
f : X → Y
hf : IsEmbedding f
_i : T2Space X
q : Y
hy : range f = {q}ᶜ
this : Tendsto f (coclosedCompact X) (𝓝 q)
⊢ (fun p ↦ p.elim q f) ((fun q_1 ↦ if hq : q_1 = q then ∞ else ↑(Exists.choose ⋯)) q) = q

pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
⊢ (fun p ↦ p.elim y f) ((fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) q) = q

Tactic:
·

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
f : X → Y
hf : IsEmbedding f
_i : T2Space X
q : Y
hy : range f = {q}ᶜ
this : Tendsto f (coclosedCompact X) (𝓝 q)
⊢ (fun p ↦ p.elim q f) ((fun q_1 ↦ if hq : q_1 = q then ∞ else ↑(Exists.choose ⋯)) q) = q
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
⊢ (fun p ↦ p.elim y f) ((fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) q) = q

Tactic:
·

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : q ≠ y
⊢ (fun p ↦ p.elim y f) ((fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) q) = q
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : a = ⊤
⊢ ℝ → ℝ

pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : a = ⊤
⊢ ℝ → ℝ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x‖⁻¹) 0 R = circleAverage (fun x ↦ log ‖f x‖) 0 R

pp: case hf₁
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 R

pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
·

Goal state after:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x‖⁻¹) 0 R = circleAverage (fun x ↦ log ‖f x‖) 0 R
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 R

pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
·

Goal state after:
case hf₁
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 R
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
·

Goal state after:
case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
⊢ 0 ≤ proximity f a
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
⊢ 0 ≤ proximity f a
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

pp: case neg
g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
·

Goal state after:
case pos
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r

pp: case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
·

Goal state after:
case hf₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

pp: case neg
g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
· suffices {h | 0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
    exact isOpen_Ioi (a := (0 : ℝ)) |>.preimage (by fun_prop) |>.mem_nhds hg

Goal state after:
case neg
g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
·

Goal state after:
case neg
g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
·

Goal state after:
case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
·

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case inl
hK : IsCompact ∅
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ ∅ → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

Tactic:
·

Goal state after:
case inl
hK : IsCompact ∅
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ ∅ → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r

pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

pp: case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
·

Goal state after:
case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

pp: case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
·

Goal state after:
case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
·

Goal state after:
case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖) 0 r

pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₂ x‖) 0 r

Tactic:
·

Goal state after:
case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖) 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₂ x‖) 0 r

Tactic:
·

Goal state after:
case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₂ x‖) 0 r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case «0»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨0, ⋯⟩) j| ≤ max √A √A'

pp: case «1»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ max √A √A'

Tactic:
·

Goal state after:
case «0»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨0, ⋯⟩) j| ≤ max √A √A'
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card

pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
·

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
·

Goal state after:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case pos
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

pp: case neg
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : ¬R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
·

Goal state after:
case pos
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case neg
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : ¬R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
·

Goal state after:
case neg
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : ¬R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case «1»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ max √A √A'

Tactic:
·

Goal state after:
case «1»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ max √A √A'
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ (↑(D₁ 0) + ↑(D₂ 0)) * log r = ↑(D₁ 0) * log r + ↑(D₂ 0) * log r

Tactic:
·

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ CircleIntegrable |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| 0 r

pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| x ≤ log⁺ ‖a₀‖ + log 2

Tactic:
·

Goal state after:
case hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ CircleIntegrable |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| 0 r
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| x ≤ log⁺ ‖a₀‖ + log 2

Tactic:
·

Goal state after:
case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| x ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2