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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
by
  classical
  exact Nat.find_spec (K.exists_mem x)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMinOrder α
s : Set α
h₁ : upperClosure s = ⊥
h₂ : BddBelow s
⊢ False

Tactic:
by simpa [h₁] using bddBelow_upperClosure.mpr 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)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hKc : ∀ (i : ι), IsCompact (K i)
htK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst✝] u
v : Set X
hv : IsOpen[inst✝] v
x✝ : X
hxs✝ : x✝ ∈ s
hxu✝ : ⟨x✝, hxs✝⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty

Tactic:
exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ (∀ x_1 ∈ s, ContinuousWithinAt (update f x y) s x_1) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))

Tactic:
← and_forall_ne x,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ ((x ∈ s → ContinuousWithinAt (update f x y) s x) ∧ ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})

Tactic:
exact ih.sdiff_singleton _

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α

Tactic:
· rw [locallyConnectedSpace_iff_connectedComponentIn_open]
    refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
    rw [connectedComponentIn_eq hy]
    rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
    exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty) i j
⊢ IsPreconnected (⋃ n, s n)

Tactic:
rw [← biUnion_univ]
  exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
    simpa [mem_univ] using K i j

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty

Tactic:
exact h3 hj hi hk

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

Goal state before:
pp: case refine_1.inl.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' inl ⁻¹' s

Tactic:
· exact (image_preimage_eq_of_subset h).symm

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

Goal state before:
pp: case refine_1.inr.refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' inr ⁻¹' s

Tactic:
· exact (image_preimage_eq_of_subset h).symm

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∩ s ∪ v' ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
← union_inter_distrib_right

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ x✝ ∈ Subtype.val '' t → x✝ ∈ s

Tactic:
simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]

Goal state after:
case left
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Set ↑s
htc : t.Countable
htsub : s ⊆ ⋃ x ∈ t, U ↑x
x✝ : X
⊢ ∀ (x : x✝ ∈ s), ⟨x✝, ⋯⟩ ∈ t → x✝ ∈ s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
⊢ s ⊆ u

Tactic:
by
  have A : s ⊆ u ∪ (closure u)ᶜ := by
    intro x hx
    by_cases xu : x ∈ u
    · exact Or.inl xu
    · right
      intro h'x
      exact xu (h (mem_inter h'x hx))
  apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u
  exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
l : Filter X
inst✝ : CountableInterFilter l
hs : IsLindelof s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen[inst✝¹] (U x)
t : Set X
htc : t.Countable
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ ⋂ i ∈ t, (U i)ᶜ ∈ l

Tactic:
exact (countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h :
  ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝] (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
⊢ f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

Tactic:
by
  contrapose! h
  simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h
  choose fsub U hU hUf using h
  refine ⟨s, U, fun x ↦ (hU x).2, fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1 ⟩, ?_⟩
  intro t ht h
  have uinf := f.sets_of_superset (le_principal_iff.1 fsub) h
  have uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f := (countable_bInter_mem ht).mpr (fun _ _ ↦ hUf _)
  rw [← compl_iUnion₂] at uninf
  have uninf := compl_notMem uninf
  simp only [compl_compl] at uninf
  contradiction

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
⊢ s ⊆ u ∩ s ∪ v ∩ s

Tactic:
← union_inter_distrib_right

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
⊢ s ⊆ (u ∪ v) ∩ s
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: 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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
by_cases hxu : x ∈ u

Goal state after:
case pos
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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

case neg
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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α

Tactic:
intro V V_in

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
      let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
      have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩
      have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
      simp [this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
⊢ UniformCauchySeqOnFilter F p p'

Tactic:
by
  intro u hu
  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
  have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
  apply this.diag_of_prod_right.mono
  simp only [and_imp, Prod.forall]
  intro n1 n2 x hl hr
  exact htmem <| SetRel.prodMk_mem_comp (htsymm hl) hr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n ↦ F (u n)) f atTop

Tactic:
simp_rw [← tendstoUniformlyOn_univ]
  exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t

Tactic:
by
      rcases U_le s hs with ⟨m, hm⟩
      rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩
      refine
        ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩
      · have := le_max_left m n
        exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm
      · exact hm (hn _ <| le_max_right m n)

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

Goal state before:
pp: case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ (∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K

Tactic:
rintro ⟨i, hpi, hi⟩

Goal state after:
case mpr
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SecondCountableTopology α
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
obtain ⟨B, hB, _⟩ := has_seq_basis α
  replace hs (n : ℕ) := hs (B n) (hB.mem n)
  choose t tC ht using hs
  have := fun n => (tC n).to_subtype
  choose o hox hos using fun (n : ℕ) (x : t n) (hx : (ball x.1 (B n) ∩ s).Nonempty) => hx
  refine ⟨⋃ (n) (x), range (o n x), iUnion₂_subset fun _ _ => range_subset_iff.2 (hos _ _),
    countable_iUnion fun _ => countable_iUnion fun _ => countable_range _, fun x hx => ?_⟩
  rw [mem_closure_iff_ball]
  intro U hU
  obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU
  obtain ⟨n, hn⟩ := hB.mem_iff.1 hV
  specialize ht n hx
  rw [mem_iUnion₂] at ht
  obtain ⟨y, hy, hyx⟩ := ht
  refine ⟨o n ⟨y, hy⟩ ⟨x, hyx, hx⟩, ?_, ?_⟩
  · apply ball_mono ((SetRel.comp_subset_comp hn hn).trans hVU)
    exact mem_ball_comp (mem_ball_symmetry.2 hyx) (hox n ⟨y, hy⟩ ⟨x, hyx, hx⟩)
  · exact mem_iUnion₂_of_mem ⟨y, hy⟩ (mem_range_self ⟨x, hyx, hx⟩)

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ |max a c - max b c| ≤ |a - b|

Tactic:
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
    using abs_max_sub_max_le_max a c b c

Goal state after:
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 ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ TendstoLocallyUniformlyOn G f p s

Tactic:
by
  have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2) := by
    simpa using eventually_prod_principal_iff.2 hg
  rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
  refine forall₂_imp (fun x hx hf => ?_) hf
  rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
  exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((Inseparable.rfl.prod hg).mem_open_iff hi.2).1 hf)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ 𝓤 (α →ᵤ β) ≤ comap (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 β)

Tactic:
(UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
    UniformSpace.comap_comap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖,
      UniformSpace.comap ((fun x ↦ f ∘ x) ∘ ⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑s) β) =
    ⨅ i ∈ 𝔖,
      UniformSpace.comap ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) ∘ fun x ↦ f ∘ x)
        (UniformFun.uniformSpace (↑i) β)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)

Tactic:
rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space (G ⧸ N) ↔ IsClosed[inst✝²] ↑N

Tactic:
by
  rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
      isClosed_coinduced]
  rfl

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ connectedComponent g = {g}

Tactic:
rw [← mul_one g, ← smul_connectedComponent, h, Set.smul_set_singleton, smul_eq_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 ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)

Tactic:
by
  refine ⟨?_, Tendsto.mul_const b⟩
  convert! Tendsto.mul_const b⁻¹ using 3 <;> rw [mul_inv_cancel_right]

Goal state after:
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
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ ↑n

Tactic:
zpow_natCast

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ n
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ WeaklyLocallyCompactSpace G

Tactic:
refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩

Goal state after:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ

Tactic:
· refine iUnion_eq_univ_iff.2 fun x => ?_
    obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty := by
      rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
      exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
    exact ⟨n, hn⟩

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ Disjoint K (g • L)

Tactic:
refine disjoint_left.2 fun a ha h'a => hg ?_

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
⊢ g ∈ K * L⁻¹
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f g : A →ₜ* B
h : f.toContinuousMap = g.toContinuousMap
⊢ ∀ (x : A), f x = g x

Tactic:
by convert! DFunLike.ext_iff.1 h

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f g : A →ₜ* B
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (x : A), f x = g x

Tactic:
by convert! DFunLike.ext_iff.1 h

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

Goal state before:
pp: case inl
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x

pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Tactic:
· exact h hx

Goal state after:
case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x