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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ (a : X) (b : Y), (a, b) ∈ s → s ∈ 𝓝 (a, b)) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
mem_nhds_prod_iff',

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
⊢ (∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ a ∈ u ∧ IsOpen[inst✝] v ∧ b ∈ v ∧ u ×ˢ v ⊆ s) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
by
  rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a

Tactic:
rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s.Nonempty → sᶜ.Finite

Tactic:
by
  simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
    WithTopology.preimage_toTopology, image_nonempty,
    finite_image_iff (WithTopology.ofTopology_injective _).injOn]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ᶠ (x : α) in 𝓝 ↑a, (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J

Tactic:
apply Eventually.of_forall

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ∀ (x : α), (∃ a, ↑a = x ∧ a ∈ J) ↔ ∃ a, ↑a = x ∧ ∃ (h : ↑a ∈ s), ⟨↑a, h⟩ ∈ J
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝] t
u : Set α
hu : IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed[inst✝¹] (f ⁻¹' t ∩ s)

Tactic:
hu.2

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝] t
u : Set α
hu : IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed[inst✝¹] (u ∩ s)
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]
    exact isOpenMap_fst.comp h

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Tactic:
· refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_
    rwa [ht.closure_eq]

Goal state after:
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
this : ∃ m, x ≤ m ∧ Maximal (fun x_1 ↦ x_1 ∈ Ico x ⊤) m
⊢ ∃ a, IsCoatom a ∧ x ≤ a

pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub

Tactic:
· obtain ⟨y, hxy, hmax⟩ := this
    refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
    exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
c : Set α
hxc : c ⊆ Ico x ⊤
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ico x ⊤, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
rwa [compl_compl]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]
    exact isOpen_empty

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
⊢ MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)

Tactic:
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
rw [hf.1]

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace β
inst✝ : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ K', IsCompact K' ∧ K ⊆ interior K'

Tactic:
by
  choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x
  rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩
  refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩
  exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
rw [hf.1]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
⊢ s.Finite

Tactic:
have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Finite
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ IsCompact s

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds', hTS]

Goal state after:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact univ

Tactic:
rw [← hf'.range_eq]

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact (range f)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization sᶜ → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
stableUnderSpecialization_iff_exists_sUnion_eq

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor <;> intro H

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hK : ∀ (i : ι), IsCompact (K i)
hsK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ K, IsCompact K ∧ s ⊆ K

Tactic:
exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

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:
by
  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.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
constructor <;> intro H

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
⊢ IsPreirreducible S

Tactic:
intro a b ha hb ⟨p, pS, pa⟩ bS

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
⊢ (S ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
by
  refine ⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩
  obtain ⟨-, hx, x, rfl⟩ := h
  exact ⟨x, hx⟩

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
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ s ⊆ closure[inst✝¹] (f '' f ⁻¹' s)

Tactic:
refine subset_trans (subset_closure_inter_of_isPreirreducible_of_isOpen hs h.isOpen_range ?_) ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ (s ∩ range f).Nonempty

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ closure[inst✝¹] (s ∩ range f) ⊆ closure[inst✝¹] (f '' f ⁻¹' s)
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
⊢ SeparatedNhds s t

Tactic:
have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
  -- we split `s` into its frontier and its interior.
  rw [← sdiff_union_of_subset (interior_subset (s := s))]
  -- since `t ⊆ sᶜ`, which is open, and `interior s` is open, we have
  -- `SeparatedNhds (interior s) t`, which leaves us only with the frontier.
  refine .union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
    H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩
  -- Since the frontier of `s` is compact (as it is a subset of `closure sᶜ`), we simply apply
  -- `SeparatedNhds_of_isCompact_isCompact`.
  rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]
  refine .of_isCompact_isCompact_isClosed ?_ ht H3 (disjoint_of_subset_left inter_subset_left H4)
  exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

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

Goal state before:
pp: ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s ↔ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor <;> intro H

Goal state after:
case mp
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsCompact s
⊢ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
⊢ x ∈ t

Tactic:
by_contra hxt

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
hxt : x ∉ t
⊢ False
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : x ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug
⊢ f x ≠ g x

Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage] at hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
⊢ f x ≠ g x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ univ \ {x} ∈ 𝓝[≠] z ∧ univ \ {x} ∩ (s \ {x}ᶜ) = ∅

Tactic:
exact ⟨nhdsNE_of_nhdsNE_sdiff_finite univ_mem Finite.of_subsingleton, by aesop⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ Disjoint (𝓝ˢ K) (𝓝ˢ L)

Tactic:
hK.disjoint_nhdsSet_left,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, Disjoint (𝓝 x) (𝓝ˢ L)
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
c : ConnectedComponents α
⊢ IsOpen {c}

Tactic:
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe c

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen {ConnectedComponents.mk x}
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ False

Tactic:
rw [not_disjoint_iff_nonempty_inter] at hsv

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : (insert i I).piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
Finset.piecewise_insert

Goal state after:
case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
⊢ s.Countable

Tactic:
have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Countable
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
⊢ u = ⋃ x ∈ u, connectedComponentIn v x

Tactic:
have := congr(((↑) : Set v → Set X) $(hu.biUnion_connectedComponent_eq.symm))
  simp only [Subtype.image_preimage_coe, mem_preimage, iUnion_coe_set, image_val_iUnion,
    inter_eq_right.mpr huv₁] at this
  nth_rw 1 [this]
  congr! 2 with x hx
  simp only [← connectedComponentIn_eq_image]
  exact le_antisymm (iUnion_subset fun _ ↦ le_rfl) <|
    iUnion_subset fun hx ↦ subset_iUnion₂_of_subset (huv₁ hx) hx le_rfl

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
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)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
x : X
hx : x ∈ s
⊢ x ∈ U ∩ e

Tactic:
exact hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      (((∀ t ∈ compl '' x, IsOpen[inst✝] t) ∧ ∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable) ∧
        ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S

Tactic:
← forall_and,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, ((∀ x_1 ∈ compl '' x, IsOpen[inst✝] x_1 ∧ Dense x_1) ∧ (compl '' x).Countable) ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Connected.Clopen

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

Tactic:
right
    rw [Subset.antisymm_iff] at T₂_v
    suffices f ⁻¹' t ⊆ f ⁻¹' T₂
      from (this.trans T₂_v.1).trans inter_subset_right
    exact preimage_mono h

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
⊢ ¬IsMeagre s

Tactic:
intro h
  rcases mem_residual.1 h with ⟨t, hts, htG, hd'⟩
  rcases (hd.inter_of_Gδ hs htG hd').nonempty with ⟨x, hx₁, hx₂⟩
  exact hts hx₂ hx₁

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : U ∈ UniformSpace.uniformity
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity

Tactic:
exact preimage_mem_comap hU

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
⊢ 𝓟 SetRel.id ≤ UniformSpace.uniformity

Tactic:
by
    rintro U hU ⟨x, y⟩ (rfl : x = y)
    have : Prod.mk x ⁻¹' U ∈ 𝓝 x := by
      rw [UniformSpace.nhds_eq_comap_uniformity]
      exact preimage_mem_comap hU
    convert! mem_of_mem_nhds 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 : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ TendstoUniformlyOn F g p s

Tactic:
tendstoUniformlyOn_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ Tendsto (fun q ↦ (g q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)