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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (f ⁻¹' (s ∩ Z))

Tactic:
rw [hf.isCompact_preimage_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (s ∩ Z)

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ s ∩ Z ⊆ range f
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
exact @hs _ hf inf_le_right

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ upperClosure s = ⊤ ↔ s = ∅

Tactic:
rw [eq_top_iff, le_upperClosure]; simp

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (s.sigma t)

Tactic:
by
  rw [Set.sigma_eq_biUnion]
  exact hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)

Tactic:
apply le_antisymm

Goal state after:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' s)

Tactic:
rw [← compl_compl s, preimage_compl]
      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓝[s] p = 𝓟 ({x | x ⤳ p} ∩ s)

Tactic:
apply le_antisymm

Goal state after:
case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓝[s] p ≤ 𝓟 ({x | x ⤳ p} ∩ s)

case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 ({x | x ⤳ p} ∩ s) ≤ 𝓝[s] p
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
⊢ IsOpen[inst✝¹] {x}

Tactic:
have C : (s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst✝¹] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
⊢ Disjoint (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
⊢ closure[inst✝¹] K \ U ∩ (closure[inst✝¹] K \ V) = ∅
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

Tactic:
intro hd hbot

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ False
Module: Mathlib.Topology.Clopen

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a ∩ (s ∩ b) = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
this : (t ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inr.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (inl '' t)
h : (inl '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inl '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inl '' t = inr '' t_1

Tactic:
exact Or.inl ⟨t, ht.isPreconnected, rfl⟩

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f

Tactic:
exact hf x hx

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Tactic:
intro u v hu hv hs hsu hsv
    by_contra H
    specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)
    apply H
    rcases h with h | h
    · rcases hsv with ⟨x, hxs, hxv⟩
      exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
    · rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ u ∩ s ∩ (v ∩ s) = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
hx : x ∈ F
h : y ∈ Subtype.val '' connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y

Tactic:
obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F ↑⟨y, hy⟩
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ f x = f y

Tactic:
suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ F ⟨x, hx⟩ = F ⟨y, hy⟩
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ Disjoint (f ⁻¹' t ∩ u) (f ⁻¹' t ∩ v)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ f ⁻¹' t ∩ u ∩ (f ⁻¹' t ∩ v) = ∅
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ Disjoint (u ∪ v)ᶜ (⋂ U ∈ si, ↑U)

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
case refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ (u ∪ v)ᶜ ∩ ⋂ U ∈ si, ↑U = ∅
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
s N : Set X
⊢ SetRel.id.IsCover s N ↔ s ⊆ N

Tactic:
by simp [IsCover, subset_def]

Goal state after:
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝ : DiscreteUniformity X
⊢ ⊥.toTopologicalSpace = ⊥

Tactic:
UniformSpace.toTopologicalSpace_bot

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝ : DiscreteUniformity X
⊢ ⊥ = ⊥
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t

Tactic:
obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]
  refine (atTop_basis.prod_self.tendsto_iff h).trans ?_
  simp only [true_and, Prod.forall, mem_prod_eq,
    mem_Ici, and_imp, Prod.map, @forall_comm (_ ≤ _) β]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
U : Set α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)

Tactic:
simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU]
    using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)

Tactic:
exact hx.mem_closure_of_mem _ hst

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ ⊥.TotallyBounded

Tactic:
rw [← principal_empty, totallyBounded_principal_iff]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded ∅
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ map f (mk a) = mk (f a)

Tactic:
by
  rw [map, lift'_mk (uniformContinuous_mk.comp h)]; rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: β : Type v
inst✝¹ : UniformSpace β
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology β
f : α → β
⊢ UniformContinuous f

Tactic:
by
  rw [UniformContinuous, eq_top_uniformSpace (α := β), top_uniformity]
  exact Filter.tendsto_top

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 SetRel.id

Tactic:
by
  refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))
  calc
    comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
    _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
    _ ≤ 𝓟 SetRel.id := principal_mono.2 ?_
  rintro ⟨x, y⟩; simpa [not_imp_not] using @hf x y

Goal state after:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst✝¹] K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ K

Tactic:
← h'K.closure_eq

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst✝¹] K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ closure[inst✝¹] K
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ (x : α), (¬∃ b ∈ t, (x, b) ∈ s) → ∀ᶠ (y : α) in nhds x, ¬∃ b ∈ t, (y, b) ∈ s

Tactic:
not_exists,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ (x : α), (∀ (x_1 : β), ¬(x_1 ∈ t ∧ (x, x_1) ∈ s)) → ∀ᶠ (y : α) in nhds x, ∀ (x : β), ¬(x ∈ t ∧ (y, x) ∈ s)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : TopologicalSpace α
inst✝ : DivisionMonoid β
f : α → β
hf : HasCompactMulSupport f
⊢ HasCompactMulSupport f⁻¹

Tactic:
by
  simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv] using hf

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (Equiv.ofInjective f ⋯).invFun

Tactic:
rw [hf.isUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe,
      Equiv.self_comp_ofInjective_symm]

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous Subtype.val
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
⊢ TendstoLocallyUniformlyOn F f p s

Tactic:
refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_
  obtain ⟨t, ht, htr⟩ := h x hx
  rw [tendstoUniformlyOn_iff_tendsto] at htr
  exact htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀

Tactic:
simp only [EquicontinuousAt, forall_subtype_range_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
  rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : β × β) in 𝓤 β, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x ↦ u ∘ x) ∘ F) S

Tactic:
by
  have := UniformFun.postcomp_isUniformInducing (α := ι) hu
  simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff]
  rfl

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (fun x ↦ a * x) '' Ioi 0 = Ioi 0

Tactic:
by
  rw [image_mul_left_Ioi ha, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]

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

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ b * f x) l (𝓝 (b * c)) → Tendsto f l (𝓝 c)

Tactic:
convert! Tendsto.const_mul b⁻¹ using 3

Goal state after:
case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
x✝ : α
⊢ f x✝ = b⁻¹ * (b * f x✝)

case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ b * f x) l (𝓝 (b * c))
⊢ c = b⁻¹ * (b * c)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ (f x)⁻¹

Tactic:
have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x ↦ 1 / f x
⊢ UniformContinuous fun x ↦ (f x)⁻¹