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✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] (f ⁻¹' s)

Tactic:
]

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] (f ⁻¹' s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty.infty
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Inseparable ∞ ∞ ↔ ∞ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty.coe
X : Type u_1
inst✝ : TopologicalSpace X
x✝ : X
⊢ Inseparable ∞ ↑x✝ ↔ ∞ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.infty
X : Type u_1
inst✝ : TopologicalSpace X
x✝ : X
⊢ Inseparable ↑x✝ ∞ ↔ ↑x✝ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.coe
X : Type u_1
inst✝ : TopologicalSpace X
x✝¹ x✝ : X
⊢ Inseparable ↑x✝¹ ↑x✝ ↔ ↑x✝¹ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ↑x✝¹ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (insert none (range Option.some))

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (insert none (range Option.some))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[inst✝¹] {x✝} ∧ IsCompact {x✝}

Tactic:
]

Goal state after:
case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[inst✝¹] {x✝} ∧ IsCompact {x✝}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
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 := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)

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 := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)
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.Compactification.OnePoint.Basic

Goal state before:
pp: case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ IsOpen[inst✝¹] (some ⁻¹' {y})

pp: case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ ∞ ∉ {y}

Tactic:
]

Goal state after:
case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ IsOpen[inst✝¹] (some ⁻¹' {y})

case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ ∞ ∉ {y}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ IsOpen[inst✝¹] (some ⁻¹' {↑val})

pp: case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ ∞ ∉ {↑val}

Tactic:
]

Goal state after:
case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ IsOpen[inst✝¹] (some ⁻¹' {↑val})

case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ ∞ ∉ {↑val}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: 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
⊢ ∀ t ∈ 𝓝 y, ∃ i, IsCompact i ∧ MapsTo f iᶜ t

Tactic:
]

Goal state after:
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
⊢ ∀ t ∈ 𝓝 y, ∃ i, IsCompact i ∧ MapsTo f iᶜ t
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: 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
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ IsCompact Uᶜ

Tactic:
]

Goal state after:
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
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ IsCompact Uᶜ
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsClosed[x✝²] (f ⁻¹' (s ∩ range f))

Tactic:
]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsClosed[x✝²] (f ⁻¹' (s ∩ range f))
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsOpen[x✝²] (f ⁻¹' (s ∩ range f))

Tactic:
]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsOpen[x✝²] (f ⁻¹' (s ∩ range f))
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

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

case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst✝¹] (Subtype.val '' Subtype.val ⁻¹' s)

Tactic:
]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst✝¹] (Subtype.val '' Subtype.val ⁻¹' s)
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 : ℂ
hx : x ∈ sphere 0 |r|
⊢ log⁺ ‖∑ c ∈ s, f c x‖ ≤ log ↑s.card + ∑ c ∈ s, log⁺ ‖f c x‖

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 : ℂ
hx : x ∈ sphere 0 |r|
⊢ log⁺ ‖∑ c ∈ s, f c x‖ ≤ log ↑s.card + ∑ c ∈ s, log⁺ ‖f c x‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I) ≤ 1 / δ
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ

Tactic:
]

Goal state after:
case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I) ≤ 1 / δ
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: 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
⊢ 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 + circleAverage (fun x ↦ log ↑s.card) 0 r

Tactic:
]

Goal state after:
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
⊢ 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 + circleAverage (fun x ↦ log ↑s.card) 0 r
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: 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
⊢ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r =
    circleAverage ((∑ i ∈ s, fun x ↦ log⁺ ‖f i x‖) + fun x ↦ log ↑s.card) 0 r

Tactic:
]

Goal state after:
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
⊢ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r =
    circleAverage ((∑ i ∈ s, fun x ↦ log⁺ ‖f i x‖) + fun x ↦ log ↑s.card) 0 r
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
apply compactlyGeneratedSpace_of_isClosed_of_t2

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
⊢ ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)) → IsClosed[inst✝³] s
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ g • I ∈ K

Tactic:
]

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ g • I ∈ K
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 0 ^ 2 + !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1 ^ 2 =
    !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 0 ^ 2 +
      !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 1 ^ 2

Tactic:
]

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 0 ^ 2 + !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1 ^ 2 =
    !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 0 ^ 2 +
      !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 1 ^ 2
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
]

Goal state after:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity f₁ 0 + proximity f₂ 0 = proximity f₁ 0 + proximity f₂ 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' (s ∩ K))

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' (s ∩ K))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ n • proximity f⁻¹ ⊤ = n • proximity f⁻¹ ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

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

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 R - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    circleAverage (fun x ↦ log ‖f x‖) 0 R - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall 0 |R|)) u) * log (R * ‖0 - u‖⁻¹) + ↑((divisor f (closedBall 0 |R|)) 0) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖ -
      Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall 0 |R|)) u) * log (R * ‖0 - u‖⁻¹) + ↑((divisor f (closedBall 0 |R|)) 0) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖ -
      Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) 0 =
    circleAverage (fun x ↦ log ‖f x‖) 0 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ) 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)

Tactic:
]

Goal state after:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + proximity f₂ ⊤ r + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r)

Tactic:
]

Goal state after:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + proximity f₂ ⊤ r + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r)