mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow ↑(upperClosure s) ↔ BddBelow s

Tactic:
BddBelow,

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ (lowerBounds ↑(upperClosure s)).Nonempty ↔ (lowerBounds s).Nonempty
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) ≤ 𝓝 (f y)

Tactic:
calc pure (f x)
    _ = map f (pure x) := (map_pure f x).symm
    _ ≤ map f (𝓝 y ⊓ 𝓟 s) := map_mono (le_inf h ((pure_le_principal x).mpr hx))
    _ = map f (𝓝[s] y) := rfl
    _ ≤ _ := hf.tendsto

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (f '' closure[inst✝¹] {x})

Tactic:
(specializingMap_iff_closure_singleton hf).mp h x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (closure[inst✝] {f x})
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : GeneralizingMap f
hg : GeneralizingMap g
⊢ GeneralizingMap (g ∘ f)

Tactic:
simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *
  exact fun s h ↦ hg _ (hf _ h)

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ (Filter.coprodᵢ fun d ↦ cocompact (X d)) = cocompact ((d : ι) → X d)

Tactic:
refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_
  refine compl_surjective.forall.2 fun s H => ?_
  simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢
  choose K hKc htK using H
  exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩

Goal state after:
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a

Tactic:
simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ interior s = s ↔ frontier s = ∅

Tactic:
frontier,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ interior s = s ↔ closure[inst✝] s \ interior s = ∅
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
⊢ LocallyConnectedSpace β

Tactic:
refine locallyConnectedSpace_of_connected_bases (fun _ s ↦ f ⁻¹' s)
    (fun x s ↦ (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) (fun x ↦ ?_)
    (fun x s hxs ↦ hxs.1.2.2.isPreconnected.preimage_of_isOpenMap h.injective h.isOpenMap hxs.2)

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ (𝓝 x).HasBasis (fun s ↦ (IsOpen[inst✝²] s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) fun s ↦ f ⁻¹' s
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊔ l₂)

Tactic:
refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₁

case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
⊢ ⋂₀ S ∈ l₂
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊔ l₂)

Tactic:
refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩ <;> refine (countable_sInter_mem hSc).2 fun s hs => ?_

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁

case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.superset
α : Type u_2
g : Set (Set α)
s s✝ t✝ : Set α
a✝¹ : CountableGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s✝
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ t✝

Tactic:
refine Exists.imp (fun S => ?_) ih

Goal state after:
case mp.superset
α : Type u_2
g : Set (Set α)
s s✝ t✝ : Set α
a✝¹ : CountableGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s✝
S : Set (Set α)
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s✝ → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t✝
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize h u v hu hv hs

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ B, x ∈ t ∧ closure[inst✝¹] t ⊆ s

Tactic:
by
  simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize h u v hu hv hs

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
simp_rw [connectedComponentIn_eq_image hx] at h ⊢

Goal state after:
α : 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
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α

Tactic:
· rintro ⟨x, h⟩
    have : PreconnectedSpace α :=
      ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
    exact ⟨⟨x⟩⟩

Goal state after:
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)
⊢ IsPreconnected (f ⁻¹' t)

Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hT]

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 α), IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
⊢ TotallyDisconnectedSpace (ConnectedComponents α)

Tactic:
totallyDisconnectedSpace_iff_connectedComponent_singleton

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i : ι
x : ConnectedComponents ↑(U i)
j : ι
y : ConnectedComponents ↑(U j)
⊢ (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        ⟨i, x⟩ =
      (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        ⟨j, y⟩ →
    ⟨i, x⟩ = ⟨j, y⟩

pp: case refine_2
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x : ConnectedComponents α
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        a =
      x

Tactic:
· intro hxy
    obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe x
    obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y
    replace hxy : ConnectedComponents.mk x.val = ConnectedComponents.mk y.val := hxy
    rw [ConnectedComponents.coe_eq_coe] at hxy
    obtain rfl : i = j := by
      apply hdisj.eq
      rw [Set.not_disjoint_iff]
      exact ⟨x, x.2, (hclopen j).connectedComponent_subset y.2 (hxy ▸ mem_connectedComponent)⟩
    simp [← Set.image_val_inj, heq, hxy]

Goal state after:
case refine_2
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x : ConnectedComponents α
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => Quotient.lift (mk ∘ Subtype.val) ⋯ x)
        a =
      x
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

Tactic:
exact u_op.preimage continuous_subtype_val

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, s ∈ comap (Prod.mk x) (𝓤 α)) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ comap (Prod.mk x) (𝓤 α) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s ↦ g (ball x s)

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (comap (Prod.mk x) (𝓤 α)).lift g = (𝓤 α).lift fun s ↦ g (ball x s)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (comap (Prod.mk c) (𝓤 β)) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ diagonal α ∈ (fun u ↦ 𝓤 α) u

Tactic:
diagonal_eq_univ

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ univ ∈ (fun u ↦ 𝓤 α) u
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔
    (∀ (a b : α), (∀ s ∈ 𝓤 α, (a, b) ∈ s) → (a, b) ∈ diagonal α) ∧ ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s

Tactic:
mem_diagonal_iff,

Goal state after:
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ↔
    (∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y) ∧ ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| 𝓝 x

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap (Prod.mk x) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (comap (Prod.mk a) (𝓤 α)) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (𝓤 ↑t) = 𝓤 ↑s

Tactic:
rw [uniformity_subtype, uniformity_subtype, comap_comap]; rfl

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ 𝓝 x
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ Filter.comap (Prod.mk x) (𝓤 α)
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
Module: Mathlib.Topology.Algebra.Group.Defs

Goal state before:
pp: G✝ : Type u_1
α : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace X
G : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 / p.2

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
G✝ : Type u_1
α : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace X
G : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 * p.2⁻¹
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            {a |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                (i.domRestrict ((toFun 𝔖) a.1) ⟨a_1, b⟩, i.domRestrict ((toFun 𝔖) a.2) ⟨a_1, b⟩) ∈ V i_1} =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {uv | ∀ x ∈ s, ((toFun 𝔖) uv.1 x, (toFun 𝔖) uv.2 x) ∈ V i}

Tactic:
domRestrict_apply

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ UniformContinuous (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖))

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, iInf₂_comm (ι₂ := Set (β × β))]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ Tendsto (fun x ↦ ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2))
    (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousAt (u ∘ Subtype.val) x₀

Tactic:
rw [← equicontinuousWithinAt_univ] at hA ⊢

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ Tendsto (fun fx ↦ (toFun 𝔖) fx.1 fx.2) (𝓝 (f, x)) (𝓝 ((toFun 𝔖) (f, x).1 (f, x).2))

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ Tendsto (fun fx ↦ (toFun 𝔖) fx.1 fx.2) (𝓝 (f, x)) (comap (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2)) (𝓤 β))
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure a⁻¹ = pure b

Tactic:
inv_eq_of_mul_eq_one_right hab

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ pure b = pure b
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 b c : G₀
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun x ↦ a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
rcases ha.eq_or_lt with rfl | ha
  · simp [(nonempty_Icc.2 hbc).image_const]
  · exact image_mul_left_Icc' ha b c

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
suffices (· + b) '' (a * ·) '' Icc c d = Icc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ x + b) '' (fun x ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : ¬a = 0
⊢ (fun x ↦ x * a⁻¹) ⁻¹' [[b, c]] = (fun x ↦ x / a) ⁻¹' [[b, c]]

Tactic:
simp only [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
⊢ T1Space α ↔ IsClosed[inst✝⁴] {x}

Tactic:
refine ⟨fun H ↦ isClosed_singleton, fun hx ↦ ⟨fun y ↦ ?_⟩⟩

Goal state after:
α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsClosed[inst✝⁴] {x}
y : α
⊢ IsClosed[inst✝⁴] {y}