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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s

Tactic:
obtain ⟨y, e', rfl⟩ := hf e

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this : (⋂ i, V i ∩ Wᶜ).Nonempty
⊢ False

Tactic:
have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]

Goal state after:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this✝ : (⋂ i, V i ∩ Wᶜ).Nonempty
this : ¬⋂ i, V i ⊆ W
⊢ False
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
A : ι → Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : (i : ι) → TopologicalSpace (A i)
x y z : X
s : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
p : α → Prop
⊢ IndiscreteTopology (Subtype p)

Tactic:
simp [TopologicalSpace.indiscrete_iff_forall_inseparable, subtype_inseparable_iff]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ IsCompact (s ∩ closure[inst✝¹] sᶜ)

Tactic:
exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsIrreducible S ↔ ∃ x, S = {x}

Tactic:
rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → s_1.Finite → s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s

Tactic:
· intro τ t hτ h₁t h₂t
    have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop
    simp_all

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x

Tactic:
isDiscrete_iff_discreteTopology

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x
Module: Mathlib.Topology.Clopen

Goal state before:
pp: 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 : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ s ∩ a

Tactic:
exact ⟨hx₁, by simpa [notMem_of_mem_compl hx₂] using cover hx₁⟩

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

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

Tactic:
by
  rw [inf_eq_iInf]
  apply R1Space.iInf
  simp [*]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α

Tactic:
locallyConnectedSpace_iff_connected_basis

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ LocallyConnectedSpace ((i : ι) → X i) ↔
    IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite →
    LocallyConnectedSpace ((i : ι) → X i)
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
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
have h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t := fun hi hj hk =>
    ht.out hi hj (Ico_subset_Icc_self hk)
  have h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t := fun hi hj hk =>
    ht.out hi hj ⟨hk.1.trans <| le_succ _, succ_le_of_lt hk.2⟩
  have h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty :=
    fun hi hj hk => K _ (h1 hi hj hk) (h2 hi hj hk)
  refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_
  exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
      ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩

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

Goal state before:
pp: α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
⊢ ∃ i, range f ⊆ range (Sigma.mk i)

Tactic:
rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩

Goal state after:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
i : ι
s : Set (X i)
hs : range f = Sigma.mk i '' s
⊢ ∃ i, range f ⊆ range (Sigma.mk i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
⊢ IsPreconnected s

Tactic:
rintro u v hu' hv' huv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
u v : Set α
hu' : IsOpen[inst✝¹] u
hv' : IsOpen[inst✝¹] v
huv : s ⊆ u ∪ v
x : α
hxs : x ∈ s
hxu : x ∈ u
y : α
hys : y ∈ s
hyv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ s ⊆ connectedComponentIn F x

Tactic:
have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
  have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs
  have := this.subset_connectedComponent h2xs
  rw [connectedComponentIn_eq_image (hsF hxs)]
  refine Subset.trans ?_ (image_mono this)
  rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst✝², inst✝] f
⊢ IsConnected univ

Tactic:
← hf.range_eq

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst✝², inst✝] f
⊢ IsConnected (range f)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[inst✝] s → NormalSpace ↑s
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
let e := (closure s ∩ closure t)ᶜ

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[inst✝] s → NormalSpace ↑s
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
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
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ¬∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, ↑i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
not_forall

Goal state after:
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
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
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, hx⟩ = F ⟨y, hy⟩

Tactic:
isDiscrete_iff_discreteTopology

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : DiscreteTopology ↑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.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
p : X → Prop
⊢ (∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x

Tactic:
simp only [Filter.Eventually, mem_residual, subset_def, mem_ofPred_eq]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
p : X → Prop
⊢ (∃ t, (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
p : X → Prop
⊢ (∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x

Tactic:
simp only [Filter.Eventually, mem_residual, subset_def, mem_ofPred_eq]
  tauto

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ TopologicalSpace.induced val inst✝ ⊓ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝ =
    TopologicalSpace.induced val inst✝

Tactic:
inf_eq_left,

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ TopologicalSpace.induced val inst✝ ≤ TopologicalSpace.induced (fun u ↦ ↑u⁻¹) inst✝
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf : IsEmbedding ⇑f
⊢ IsEmbedding ⇑(map f)

Tactic:
by
  refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
  exact hf.prodMap (opHomeomorph.isEmbedding.comp <| hf.comp opHomeomorph.symm.isEmbedding)
    |>.comp isEmbedding_embedProduct

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

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝¹ : DiscreteUniformity X
Y : Type u_2
inst✝ : UniformSpace Y
f : X → Y
⊢ UniformContinuous f

Tactic:
simp only [uniformContinuous_iff_le_comap, DiscreteUniformity.eq_bot, bot_le]

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
this : Cauchy (Filter.comap Subtype.val f)
⊢ Cauchy (map m f)

Tactic:
simpa [Set.domRestrict_def, ← Function.comp_def, ← map_map,
      subtype_coe_map_comap, inf_eq_left.mpr hfs] using this.map hm.restrict

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
U : SetRel β β
inst✝ : U.IsSymm
s N : Set β
⊢ U.IsCover s N ↔ s ⊆ ⋃ y ∈ N, ball y U

Tactic:
simp [SetRel.IsCover, subset_def, ball, U.comm]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ball x V ∈ 𝓝[S] x

Tactic:
rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V
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:
simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
  rfl

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty α
f✝ : Filter β
hf : Cauchy f✝
x a : α
b : β
hab : pure x ×ˢ f✝ ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 b

Tactic:
simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ (∀ (i : ↑u₂), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔ ∀ u ∈ u₂, Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
SetCoe.forall

Goal state after:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ (∀ (x : UniformSpace β) (h : x ∈ u₂), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
    ∀ u ∈ u₂, Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)

Tactic:
delta UniformContinuousOn UniformContinuous
  rw [← map_uniformity_set_coe, tendsto_map'_iff]; rfl

Goal state after:
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:
map,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' (mk ∘ f) (mk a) = mk (f a)
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
⊢ IsUniformEmbedding f

Tactic:
let _ : UniformSpace α := ⊥

Goal state after:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x✝ : UniformSpace α := ⊥
⊢ IsUniformEmbedding f
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
inst✝ : DiscreteTopology α
⊢ IsClosedEmbedding f

Tactic:
let _ : UniformSpace α := ⊥

Goal state after:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
inst✝ : DiscreteTopology α
x✝ : UniformSpace α := ⊥
⊢ IsClosedEmbedding f
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 : α), (∀ (x_1 : β), ¬(x_1 ∈ t ∧ (x, x_1) ∈ s)) → ∀ᶠ (y : α) in nhds x, ∀ (x : β), ¬(x ∈ t ∧ (y, x) ∈ s)

Tactic:
not_and

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 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Equicontinuous F
⊢ UniformEquicontinuous F

Tactic:
rw [equicontinuous_iff_continuous] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (Prod.map ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)
        ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
      (𝓤 ((α → β) × (α → γ))) =
    𝓤 (α → β × γ)

Tactic:
← uniformity_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓤 (α → β × γ) = 𝓤 (α → β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (Prod.map Function.swap Function.swap) (𝓤 ((i : ι) → α → δ i)) = 𝓤 (α →ᵤ (i : ι) → δ i)

Tactic:
← uniformity_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ (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 → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
hxS : x ∈ S
⊢ ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
SetCoe.forall

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 → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ V
hxS : x ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy : ∀ (i : ↑A), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ U

Tactic:
SetCoe.forall

Goal state after:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)

Tactic:
rw [iInf_comm]

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ j,
      ⨅ i,
        ⨅ (_ : j ∈ 𝔖),
          UniformSpace.comap (⇑UniformFun.ofFun ∘ j.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑j) γ)