mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h

Goal state after:
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap f

Tactic:
rw [(isOpenQuotientMap_fst (Y := Z)).isOpenMap_iff]

Goal state after:
case refine_1
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap (f ∘ Prod.fst)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f (univ \ {x}) x ↔ ContinuousAt f x

Tactic:
continuousWithinAt_sdiff_self,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[instTopologicalSpaceSubtype] x✝

Tactic:
rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
    (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_val_preimage_restrictPreimage]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis (fun t ↦ t ∈ preimage f '' T ∧ a ∈ t) id

Tactic:
by
    convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
    aesop

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i

Tactic:
intro z x x' ⟨_, hz⟩

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x ⊆ ⋃ x, s x

Tactic:
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
    intro z x x' ⟨_, hz⟩
    exact ⟨x', hz⟩

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (𝓝 x ⊓ map u F).NeBot ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)

Tactic:
← Filter.push_pull',

Goal state after:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)
Module: Mathlib.Topology.Compactness.LocallyFinite

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : X → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), {i | (f i ∩ U x).Nonempty}.Finite
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ {i | (f i ∩ s).Nonempty}.Finite
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst✝] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
by
  simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
  rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ ⋃₀ (image Subtype.val '' T) = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
image

Goal state after:
α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ ⋃₀ {x | ∃ a ∈ T, Subtype.val '' a = x} = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x

Tactic:
have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩

Goal state after:
case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : x ∉ closure[inst✝²] {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact univ

Tactic:
hf.isInducing.isCompact_iff,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (f '' univ)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (A i)
f g : (i : ι) → A i
⊢ (f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i

Tactic:
by
  simp only [Inseparable, nhds_pi, funext_iff, pi_inj]

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

Goal state before:
pp: case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
x : (i : ι) × X i
⊢ ⟨x.fst, x.snd⟩ ∈ u → x.fst ∈ s

Tactic:
intro hx

Goal state after:
case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
x : (i : ι) × X i
hx : ⟨x.fst, x.snd⟩ ∈ u
⊢ x.fst ∈ s
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x y : X
hd : Disjoint (𝓝 x) (𝓝 y)
he : x = y
⊢ False

Tactic:
by simp [he, nhds_neBot.ne] at hd

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
rw [← Set.preimage_univ]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (?m.12 ⁻¹' univ)

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Type ?u.22

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Y → ?m.11
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W : ↑(irreducibleComponents X)
⊢ ↑((fun W ↦ ⟨f ⁻¹' ↑W, ⋯⟩) ((fun W ↦ ⟨f '' ↑W, ⋯⟩) W)) = ↑W

Tactic:
refine (Set.subset_preimage_image _ _).antisymm' (W.2.2 ?_ (Set.subset_preimage_image _ _))
    refine ⟨?_, (W.2.1.image _ hf₁.continuousOn).2.preimage_of_isPreirreducible_fiber _ hf₂ hf₃⟩
    obtain ⟨x, hx⟩ := W.2.1.1
    exact ⟨_, x, hx, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i ↦ max (f i) a) l (𝓝 a)

Tactic:
by
  simp_rw [max_comm _ a]
  exact h.max_right

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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen[inst✝] u
huv : Disjoint (frontier u) v
⊢ IsClopen (v ↓∩ u)

Tactic:
refine ⟨?_, isOpen_induced hu (f := Subtype.val)⟩

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen[inst✝] u
huv : Disjoint (frontier u) v
⊢ IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)
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' ∪ v'
z : α
hz : z ∈ s ∩ (s ∩ (u' ∩ v'))
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
inter_left_comm s u',

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'
z : α
hz : z ∈ s ∩ (u' ∩ (s ∩ v'))
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X

Tactic:
by
  rw [inf_eq_iInf]
  exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
⊢ ∀ V' ∈ 𝓝 (φ b), IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝 b

Tactic:
intro V' V'_in V'_closed

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen[inst✝] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
simp_rw [subset_def, mem_ofPred, forall_and, and_assoc]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

Tactic:
intro u ⟨t, tT, tu⟩
    rw [← tu]
    apply hf.isNowhereDense_image (isNowhereDense t tT)

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed[inst✝¹] (f i)
hU : s ⊆ ⋃ i ∈ t, f i
⊢ Dense (⋃ i ∈ t, interior (f i))

Tactic:
by
  have := ht.to_subtype
  simp only [biUnion_eq_iUnion, SetCoe.forall'] at *
  exact hs.dense_iUnion_interior_of_closed hd hc hU

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ ⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)

Tactic:
refine (h.continuous.continuousOn.image_connectedComponentIn_subset hx).antisymm ?_
  have := h.symm.continuous.continuousOn.image_connectedComponentIn_subset (mem_image_of_mem h hx)
  rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
cauchySeq_iff_tendsto

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ s, ball x U = univ

Tactic:
by
  refine iUnion₂_eq_univ_iff.2 fun y => ?_
  rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
  exact ⟨x, hxs, hxy⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ comap (fun x ↦ (e x.1, e x.2)) (𝓤 β)
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s

Tactic:
(uniformity_hasBasis_open_symmetric.comap _).mem_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : ∃ i, (i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i ∧ i.IsSymm) ∧ (fun x ↦ (e x.1, e x.2)) ⁻¹' id i ⊆ s
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
f : α → β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ CompleteSpace (α ⊕ β)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
  exact isUniformEmbedding_inl.isUniformInducing.isComplete_range.union
    isUniformEmbedding_inr.isUniformInducing.isComplete_range

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 α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
i : ι
⊢ Tendsto (F i) p' (𝓝 (L i)) → ∀ᶠ (x : α) in p', (F i x, L i) ∈ t

Tactic:
h2

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2✝ : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
i : ι
h2 : Tendsto (F i) p' (𝓝 (L i))
⊢ ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (range f)

Tactic:
h2

Goal state after:
case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (f '' K)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (range f)

Tactic:
h2

Goal state after:
case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (insert 1 (f '' K))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One β
inst✝ : One γ
g : β → γ
f : α → β
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ IsCompact (closure[inst✝²] (mulSupport (g ∘ f))) ↔ IsCompact (closure[inst✝²] (mulSupport f))

Tactic:
mulSupport_comp_eq g (@hg) f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
⊢ IsUniformInducing (hid.extend f)

Tactic:
have hg' : UniformContinuous (hg.extend i) :=
    uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ IsUniformInducing (hid.extend f)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (⋃ n, ⋃ x, range (o n x))

Tactic:
rw [mem_closure_iff_ball]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
  choose U hU using h V hV
  obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
  replace hU := fun x : t => (hU x).2
  rw [← eventually_all] at hU
  refine hU.mono fun i hi x => ?_
  specialize ht (mem_univ x)
  simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
  exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

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
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            {a |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                (UniformFun.toFun ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) a.1) ⟨a_1, b⟩,
                    UniformFun.toFun
                      (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖))
                          (⇑UniformFun.ofFun ∘ 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:
Prod.map_snd,

Goal state after:
α : 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),
                (UniformFun.toFun ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) a.1) ⟨a_1, b⟩,
                    UniformFun.toFun ((⇑UniformFun.ofFun ∘ 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}