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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
K : Set X
hKf : K ∈ f
hK : IsCompact K
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)

Tactic:
calc
    f ×ˢ 𝓝ˢ t
    _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ principal_le_nhdsSet
    _ = 𝓝ˢ (K ×ˢ t) := (hK.nhdsSet_prod_eq ht).symm
    _ ≤ 𝓝ˢ (Set.univ ×ˢ t) := nhdsSet_mono (prod_mono_left le_top)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl
α : 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} ∪ s ∩ {a | p a}ᶜ) x

pp: case neg.inr
α : 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} ∪ s ∩ {a | p a}ᶜ) x

Tactic:
· apply ContinuousWithinAt.union
      · exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
      · have : x ∉ closure { a | p a }ᶜ := fun h => hx' ⟨subset_closure hx.2, by
          rwa [closure_compl] at h⟩
        exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Goal state after:
case neg.inr
α : 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} ∪ s ∩ {a | p a}ᶜ) x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x x✝ : X
⊢ x✝ ∈ closure[inst✝¹] {x} ↔ x✝ ∈ (𝓝 x).ker

Tactic:
simp [ker_nhds_eq_specializes, ← specializes_iff_mem_closure, specializes_comm]

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'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = Uᶜ

Tactic:
rw [← this, compl_compl]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s = 𝓝ˢ t ↔ s = t

Tactic:
simp_rw [le_antisymm_iff]
  exact and_congr nhdsSet_le_iff nhdsSet_le_iff

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

Goal state before:
pp: case mp
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
inst✝ : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝 x] g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg

Goal state after:
case mp
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
inst✝ : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
⊢ f x = g x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst✝¹] K = ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
by
  ext; simp [hK.mem_closure_iff_exists_inseparable]

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a ⋖ b
⊢ pure b ⊔ ⊥ = pure b

Tactic:
sup_bot_eq

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a ⋖ b
⊢ pure b = pure b
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
b : α
inst✝ : PredOrder α
⊢ pure b ⊔ ⊥ = pure b

Tactic:
sup_bot_eq

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
b : α
inst✝ : PredOrder α
⊢ pure b = pure b
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ pure a ⊔ ⊥ = pure a

Tactic:
sup_bot_eq

Goal state after:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ pure a = pure a
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 α
⊢ DiscreteTopology (ConnectedComponents α)

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
  obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe c
  simp [← ConnectedComponents.isQuotientMap_coe.isOpen_preimage,
    connectedComponents_preimage_singleton, isOpen_connectedComponent]

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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ ⋂₀ S

Tactic:
mem_sInter,

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, ∀ t ∈ S, (x, y) ∈ t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
⊢ False

Tactic:
rcases isClopen_iff.mp (h_clopen i) with hi | hi

Goal state after:
case inl
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = ∅
⊢ False

case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)

Tactic:
· simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_closed j

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

Goal state before:
pp: case refine_1.insert.refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst✝] a → ∀ (b : Set α), IsOpen[inst✝] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst✝] u ∧ ∀ x ∈ U, IsOpen[inst✝] x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ⊆ ⋃₀ ↑U → ∃ x ∈ U, s ⊆ x

Tactic:
· exact IH (fun u hu => (hU.2 u hu).2) hUo.2

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst✝] U
hUs : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]

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 : (insert i I).piecewise f g ∈ u
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    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
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hne : (univ.pi s).Nonempty
hc : IsPreconnected (univ.pi s)
i : ι
⊢ IsPreconnected ((fun f ↦ f i) '' univ.pi s)

Tactic:
exact hc.image _ (continuous_apply _).continuousOn

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : Set X
hu : IsClosed[inst✝¹] u
⊢ (𝓝ˢ u).HasBasis (fun s ↦ s ∈ 𝓝ˢ u ∧ IsClosed[inst✝¹] s) id

Tactic:
refine hasBasis_self.2 fun _ ht ↦ exists_mem_nhdsSet_isClosed_subset ht hu

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

Goal state before:
pp: case inl
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
htc : ∅.Countable
htu : ∀ (i : ι), U i = ∅
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i

Tactic:
simp [htu]

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

Goal state before:
pp: case refine_1.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen[inst✝] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
exact ⟨f, by simp_all, by simp [hf]⟩

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

Goal state before:
pp: case refine_2
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
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ x ∈ ⋂ U ∈ si, ↑U

pp: case refine_3
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
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ ⋂ U ∈ si, ↑U ⊆ u ∪ v

Tactic:
· exact mem_iInter₂.2 fun s _ => s.2.2

Goal state after:
case refine_3
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
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ ⋂ U ∈ si, ↑U ⊆ u ∪ v
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
h : IsMeagre s
⊢ IsMeagre (f '' s)

Tactic:
by
  rw [isMeagre_iff_countable_union_isNowhereDense] at *
  obtain ⟨T, isNowhereDense, countable, cover⟩ := h
  refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩
  case isNowhereDense =>
    intro u ⟨t, tT, tu⟩
    rw [← tu]
    apply hf.isNowhereDense_image (isNowhereDense t tT)
  case cover =>
    rw [← Set.image_sUnion]
    grw [cover]

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
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ h x ∈ s ∧ IsConnected s) fun x ↦ ⇑h.symm '' x
x✝¹ : X
x✝ : Set Y
hs : IsOpen[inst✝] x✝ ∧ h x✝¹ ∈ x✝ ∧ IsConnected x✝
⊢ IsPreconnected (⇑h.symm '' x✝)

Tactic:
exact hs.2.2.2.image _ h.symm.continuous.continuousOn

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⁻¹
⊢ IsEmbedding val

Tactic:
refine ⟨⟨?_⟩, val_injective⟩
  rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
    @continuous_iff_continuousAt _ _ (.induced _ _)]
  intro u s hs
  simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
  exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
f : Filter α
⊢ (∀ (i' : ι), p i' → ∃ i ∈ f, id i ×ˢ id i ⊆ s i') ↔ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Tactic:
by
      simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ map Prod.swap (𝓤 α)

Tactic:
map_swap_eq_comap_swap

Goal state after:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n ↦ u (n + k)

Tactic:
· exact h.comp_tendsto (tendsto_add_atTop_nat k)

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 α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ∘
      fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')

Tactic:
simpa using! h.prodMap h'

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s i

Tactic:
rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]

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

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ u = ⊤

Tactic:
by
  refine UniformSpace.ext ?_
  rw [top_uniformity, ← Filter.ker_eq_univ]
  ext x
  rw [← inseparable_iff_ker_uniformity]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ 𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
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 ∈ 𝓤 α
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s

Tactic:
← he₁.comap_uniformity,

Goal state after:
α : 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
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
constructor
  · exact fun H f hf hfs => ⟨Ultrafilter.of f, Ultrafilter.of_le f,
      (Ultrafilter.of f).cauchy_of_totallyBounded' (H.mono ((Ultrafilter.of_le f).trans hfs))⟩
  · intro H d hd
    contrapose! H with hd_cover
    set f := ⨅ t : Finset α, g ⊓ 𝓟 (d.preimage t)ᶜ
    have hb : Antitone fun t : Finset α ↦ g ⊓ 𝓟 (d.preimage t)ᶜ :=
      fun s t (h : s ⊆ t) => by beta_reduce; gcongr
    have : Filter.NeBot f :=
      (Filter.iInf_neBot_iff_of_directed' <| hb.directed_ge).mpr fun t =>
        Filter.notMem_iff_inf_principal_compl.mp <| hd_cover t t.finite_toSet
    have : f ≤ g := iInf_le_of_le ∅ (by simp)
    refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
    rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
    rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
    have : {x | (x, y) ∈ d}ᶜ ∈ c := by
      simpa [SetRel.preimage] using hcf.trans <| (iInf_le _ {y}).trans inf_le_right
    rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, hyz⟩
    exact hyz (hmd ⟨hzm, hym⟩)

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
⊢ ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen[inst✝] u
xu : x ∈ u
⊢ ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r