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

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∉ interior {a | p a}
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))

Tactic:
rw [← mem_compl_iff, ← closure_compl] at ha

Goal state after:
case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure[inst✝²] {a | p a}
ha : a ∈ closure[inst✝²] {a | p a}ᶜ
⊢ Tendsto g (𝓝[s ∩ closure[inst✝²] {a | ¬p a}] a) (𝓝 (g a))
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a

Tactic:
ite_inter_of_inter_eq _ H

Goal state after:
case ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s s' t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst✝²] t)
h' : ContinuousOn g (s' ∩ closure[inst✝²] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ s ∩ frontier t, f a = g a
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s} → s ∈ irreducibleComponents X

Tactic:
intro H
    refine ⟨H.1.2, fun x h e => ?_⟩
    have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
    exact le_trans subset_closure this

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
⊢ IsOpen[inst✝¹] {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}

Tactic:
refine isOpen_iff_mem_nhds.mpr fun a ha => ?_
  filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb
  rcases eq_or_ne a b with rfl | h
  · exact hb
  · rw [h.symm.nhdsWithin_compl_singleton] at hb
    exact hb.filter_mono nhdsWithin_le_nhds

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
⊢ V'.Nonempty → IsClosed[inst✝¹] V' → V' = Uᶜ

Tactic:
V'ne

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
⊢ IsClosed[inst✝¹] V' → V' = Uᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun x y ↦ Disjoint (𝓝 x) (𝓝 y)

Tactic:
by
  refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)
  simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), ← exists_and_left,
    and_assoc, and_comm, and_left_comm]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ IsDiscrete (s ∪ t)

Tactic:
rw [union_eq_iUnion]
  exact .iUnion (by simp [*]) (by simp [*])

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ Disjoint (𝓝ˢ {f x}) (𝓝ˢ (f '' K \ interior s))

Tactic:
nhdsSet_singleton,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ Disjoint (𝓝 (f x)) (𝓝ˢ (f '' K \ interior s))
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}

Tactic:
rw [mem_ofPred_eq]

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ tᶜ ∈ l
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets

Tactic:
by
  constructor <;> intro h
  · exact subset_trans (fun s => CountableGenerateSets.basic) h
  intro s hs
  induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (countable_sInter_mem Sct).mpr ih

Goal state after:
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 : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
set S := update (I.piecewise f g) i '' s i

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
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
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 : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial

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
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
⊢ (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
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Countable

Tactic:
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ ⋃ x ∈ t, {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))

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsClopen (v ↓∩ u)
huv₁ : u ⊆ v
this : Subtype.val '' v ↓∩ u = Subtype.val '' ⋃ x ∈ v ↓∩ u, connectedComponent x
⊢ u = ⋃ x ∈ u, connectedComponentIn v x
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ IsTotallyDisconnected univ

Tactic:
intro s s_sub hs

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

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

Tactic:
and_assoc

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

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

Tactic:
by
  rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
  refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_
  rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ←
    connectedComponents_preimage_singleton, image_preimage_eq _ ConnectedComponents.surjective_coe]
  refine ConnectedComponents.surjective_coe.forall.2 fun y => ?_
  rw [connectedComponents_preimage_singleton]
  exact isConnected_connectedComponent

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, ((∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable) ∧ s ⊆ ⋃₀ x) ↔
    ∃ S, ((∀ t ∈ S, IsNowhereDense t) ∧ S.Countable) ∧ s ⊆ ⋃₀ S

Tactic:
and_assoc

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
constructor
  · rw [mem_residual_iff]
    rintro ⟨S, hSo, hSd, Sct, Ss⟩
    refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩
    exact dense_sInter_of_isOpen hSo Sct hSd
  rintro ⟨t, ts, ho, hd⟩
  exact mem_of_superset (residual_of_dense_Gδ ho hd) ts

Goal state after:
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
U : SetRel X X
N : Set X
⊢ U.IsCover ∅ N

Tactic:
by simp [IsCover]

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
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (f '' s)

Tactic:
← h.1.isOpen_preimage,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] (f ⁻¹' f '' s)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f

Tactic:
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

Tactic:
exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure[inst✝.toTopologicalSpace] s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ ⊤) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
inf_top_eq

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)

Tactic:
by
  refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
  rw [inseparable_iff_clusterPt_uniformity]
  exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃ i ∈ S, i) ↔ ∀ s ∈ S, TotallyBounded s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ range s ⊆ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}

Tactic:
range_subset_iff,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ y ∈ s '' {k | k ≤ n}, {x | (x, y) ∈ a}
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (f x) (f₂ x) = 1 x

Tactic:
hx,

Goal state after:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (1 x) (f₂ x) = 1 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x • f' x = 0 x

Tactic:
hx,

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x • 0 x = 0 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ f x • f' x = 0 x

Tactic:
hx,

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 x • f' x = 0 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ f x * f' x = 0 x

Tactic:
hx,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 x * f' x = 0 x
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x * f' x = 0 x

Tactic:
hx,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x * 0 x = 0 x
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
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
⊢ IsUniformInducing (SeparationQuotient.mk ∘ hg.extend i ∘ fwd)

Tactic:
key

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)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
⊢ IsUniformInducing SeparationQuotient.mk
Module: Mathlib.Topology.Coherent

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
⊢ x ∈ t

Tactic:
rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (Set X)
inst✝ : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : Subtype.val ⁻¹' s = Subtype.val ⁻¹' t
⊢ x ∈ t
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
e : α ≃ β
h₁ : UniformContinuous e.toFun
h₂ : UniformContinuous e.invFun
e' : α ≃ β
h₁' : UniformContinuous e'.toFun
h₂' : UniformContinuous e'.invFun
h :
  { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ }.toEquiv =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }.toEquiv
⊢ { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ } =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }

Tactic:
simpa only [mk.injEq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p s
hG : TendstoLocallyUniformlyOn G g p s
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *
  intro x hx
  rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff]
  exact (hF x hx).prodMk (hG x hx)

Goal state after:
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Tactic:
by
  simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]

Goal state after: