mathlib-initiative/mathlib-tactics huggingface dataset:
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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : DiscreteTopology X
f : X → Y
y : Y
h : Tendsto f cofinite (𝓝 y)
⊢ Tendsto (⇑{ toFun := f, continuous_toFun := ⋯ }) (coclosedCompact X) (𝓝 y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
⊢ IsClosed[inst✝¹] (s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
this : (∃ v ∈ g • U, v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U
⊢ g ∈ {g | (g • U ∩ V).Nonempty} ↔ g ∈ fst '' (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
f : G × G → G × X := Prod.map id fun g ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
f : G × G → G × X := Prod.map id fun g ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: P : TopCat → Prop
⊢ ∀ (X : CompHausLike P), P X.toTop → True

Tactic:
by

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

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
⊢ ProperSMul G X

Tactic:
by

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)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
⊢ (fun f ↦
        {
          toFun := fun x ↦
            match x with
            | none => Classical.choose ⋯
            | Option.some x => ↑f x,
          continuous_toFun := ⋯ })
      ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by

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

Goal state before:
pp: Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint ℕ → Y
⊢ Continuous[_, inst✝] f ↔ Tendsto (fun x ↦ f ↑x) atTop (𝓝 (f ∞))

Tactic:
by

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)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : ℕ → Y
y : Y
h : Tendsto f atTop (𝓝 y)
⊢ Tendsto f cofinite (𝓝 y)

Tactic:
by

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

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[tX] s

Tactic:
by

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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
by

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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)

Tactic:
by

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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
⊢ C(OnePoint ℕ, Y) ≃ { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MulAction G X
inst✝³ : CompactlyGeneratedSpace (X × X)
inst✝² : T2Space X
inst✝¹ : DiscreteTopology G
inst✝ : ContinuousConstSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ DenseRange some

Tactic:
by

Goal state after:
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
⊢ UCompactlyGeneratedSpace Y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
by

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) (𝓝 ∞)

Tactic:
by

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)
⊢ IsCompact univ

Tactic:
by

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)
inst✝ : T0Space X
⊢ T0Space (OnePoint X)

Tactic:
by

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)
inst✝ : T1Space X
z : OnePoint X
⊢ IsClosed[instTopologicalSpace] {z}

Tactic:
by

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)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
this : R1Space (OnePoint X)
⊢ NormalSpace (OnePoint X)

Tactic:
by

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

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
⊢ UCompactlyGeneratedSpace (X ⊕ Y)

Tactic:
by

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)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)

Tactic:
by

Goal state after:
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 atTop (𝓝 ∞)

Tactic:
by

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)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
⊢ NormalSpace (OnePoint X)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous[_, instTopologicalSpace] ⇑CofiniteTopology.of.symm

Tactic:
by

Goal state after:
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
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ Continuous[_, tX] g

Tactic:
by

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✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ univ ⊆ {↑val} ∪ {↑val}ᶜ

Tactic:
by

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✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x : OnePoint X
x✝¹ : x ∈ univ
y : OnePoint X
x✝ : y ∈ univ
hxy : x ≠ y
⊢ (fun x y ↦
      ∃ u v,
        IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v)
    x y

Tactic:
by

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

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
⊢ UCompactlyGeneratedSpace X

Tactic:
by

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)
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
⊢ MapsTo f (f ⁻¹' Uᶜ)ᶜ N

Tactic:
by

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)
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
⊢ Uᶜ ⊆ range f

Tactic:
by

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)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ Tendsto f (coclosedCompact X) (𝓝 y)

Tactic:
by

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)
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)
p : X
⊢ f p ≠ y

Tactic:
by

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)
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)
p : OnePoint X
⊢ (fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) ((fun p ↦ p.elim y f) p) = p

Tactic:
by

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)
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
⊢ q ∈ range f

Tactic:
by

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)
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
⊢ (fun p ↦ p.elim y f) ((fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) q) = q

Tactic:
by

Goal state after:
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)
⊢ IsClosed[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

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

Tactic:
by

Goal state after:
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)
⊢ IsOpen[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f ↑a₀ = circleAverage (fun x ↦ log⁺ ‖f x - a₀‖⁻¹) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f 0 = circleAverage (fun x ↦ log⁺ ‖f x‖⁻¹) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
⊢ proximity f 0 = circleAverage (fun x ↦ log⁺ ‖f⁻¹ x‖) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f ⊤ = circleAverage (fun x ↦ log⁺ ‖f x‖) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
⊢ proximity f a r = proximity g a r

Tactic:
by

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

Goal state before:
pp: X✝ : Type u
Y : Type v
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactlyGeneratedSpace (X i)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
⊢ sphere 0 |r| ⊆ univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f ↑a₀ = proximity (f - fun x ↦ a₀) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
⊢ proximity f⁻¹ ⊤ = proximity f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
⊢ Function.Even (proximity f a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : E
r : ℝ
⊢ proximity (fun x ↦ c) ⊤ r = log⁺ ‖c‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
hf : Continuous f
⊢ Continuous (proximity f ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous ↿num

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous ↿denom

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous toSL2R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: this :
  ∀ (g : SL(2, ℝ)) (τ : ℍ),
    ContinuousAt
      (fun x ↦
        match x with
        | (h, z) => (↑(↑h 0 0) * ↑z + ↑(↑h 0 1)) / (↑(↑h 1 0) * ↑z + ↑(↑h 1 1)))
      (g, τ)
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
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
⊢ CompactlyGeneratedSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | 0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : 0 < ↑(Matrix.GeneralLinearGroup.det h)
⊢ σ h = σ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | 0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ Continuous fun h ↦ ↑(Matrix.GeneralLinearGroup.det h)

Tactic:
by

Goal state after: