mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
by
    have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
hne : x ≠ y
⊢ Disjoint ((𝓝 x).lift' closure[inst✝¹]) ((𝓝 y).lift' closure[inst✝¹])

Tactic:
rw [lift'_nhds_closure, lift'_nhds_closure]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
hne : x ≠ y
⊢ Disjoint (𝓝 x) (𝓝 y)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
⊢ T25Space X

Tactic:
by
  refine ⟨fun x y hne => ?_⟩
  rw [lift'_nhds_closure, lift'_nhds_closure]
  have : x ∉ closure {y} ∨ y ∉ closure {x} :=
    (t0Space_iff_or_notMem_closure X).mp inferInstance hne
  simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this
  exact this.elim id fun h => h.symm

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F
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
hne : T.Nonempty
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)

Goal state after:
case inl
α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hne : T.Nonempty
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

case inr
α : 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
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S
Module: Mathlib.Topology.Homeomorph.Lemmas

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

Tactic:
h.preimage_image,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
⊢ u₁ = u₂

Tactic:
by
  have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h
  cases u₁; cases u₂; congr

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

Goal state before:
pp: case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
refine fun t => Monotone.set_prod ?_ monotone_const

Goal state after:
case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s ↦ {y | (y, a) ∈ s}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun i ↦ {y | (y, x) ∈ s i}

Tactic:
by
  replace h := h.comap Prod.swap
  rw [comap_swap_uniformity] at h
  exact nhds_basis_uniformity' h

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

Goal state before:
pp: case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

pp: case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
· obtain ⟨V, hV, hV'⟩ := h x hx
    exact
      ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
        (ball_mono interior_subset x).trans hV'⟩

Goal state after:
case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity]

Goal state after:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩
  rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]

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
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen[inst✝] u
xu : x ∈ u
y : β
hy : y ∈ u
⊢ (f y, g y) ∈ r

Tactic:
have I1 : (f y, f x) ∈ t := SetRel.symm t (hu hy).1

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
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
⊢ (f y, g y) ∈ r
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))

Tactic:
refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst✝ : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
obtain ⟨B, hB, _⟩ := has_seq_basis α

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t
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)
s : Set X
hsc : IsClosed[inst✝¹] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ t

Tactic:
suffices x ∈ s by specialize hst x; simp_all

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 : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ s
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
⊢ ⋂ i ∈ fs, T ↑i ⋯ ⊆ {x | x.1 ∈ s → (f x.1, f x.2) ∈ r}

Tactic:
rintro ⟨a₁, a₂⟩ h h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → a ∈ s → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → a ∈ s → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y | (f a, y) ∈ t}
fs : Finset ↑s
hsU : s ⊆ ⋃ x ∈ fs, U ↑x ⋯
a₁ a₂ : α
h : (a₁, a₂) ∈ ⋂ i ∈ fs, T ↑i ⋯
h₁ : (a₁, a₂).1 ∈ s
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i

Tactic:
exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((hg.prod .rfl).mem_open_iff hi.2).1 hf)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ UniformContinuous ⇑toFun

Tactic:
rw [uniformContinuous_pi]
  intro x
  exact uniformContinuous_eval β x

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
rw [iInf_uniformity]

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (⇑ofFun ∘ swap F) S
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) ((⨅ i, 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f

Tactic:
rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *
  exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ |b - a|

Tactic:
← max_sub_min_eq_abs

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ x + b) '' (fun x ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
Set.image_image

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ x + b) '' (fun x ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
Set.image_image

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ x + b) '' (fun x ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
Set.image_image

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ x + b) '' (fun x ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
Set.image_image

Goal state after:
K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun x ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: G₀ : Type u_5
X : Type u_6
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero X
inst✝⁴ : MulActionWithZero G₀ X
inst✝³ : TopologicalSpace G₀
inst✝² : (𝓝[≠] 0).NeBot
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul G₀ X
⊢ ⊤ • 𝓝 0 = ⊤

Tactic:
rw [(hasBasis_top.smul (basis_sets _)).eq_top_iff]
  rintro ⟨_, s⟩ ⟨-, hs⟩
  exact Set.univ_smul_nhds_zero hs

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ Ici a ^ (n + 2) = Ici (a ^ (n + 2))

Tactic:
by simp [pow_succ _ n.succ, Ici_pow_eq, Ici_mul_Ici_eq]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
⊢ Pairwise fun x y ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Tactic:
have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
⊢ Pairwise fun x y ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
⊢ Tendsto (Prod.map f g) (↑𝒰) (𝓝 (y, w)) → ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
hyw

Goal state after:
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (Prod.map f g) (↑𝒰) (𝓝 (y, w))
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b ↦ (Multiset.map (fun c ↦ f c b) s).prod) x (𝓝 (Multiset.map a s).prod)

Tactic:
by
  rcases s with ⟨l⟩
  simpa using tendsto_list_prod l

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ (IsProperMap fun x ↦ y) ↔ CompactSpace X

Tactic:
by
  classical
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  constructor
  · rintro ⟨-, -, h⟩
    exact ⟨by simpa using h y⟩
  · intro H
    refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
    simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ connectedComponent g = {g}

Tactic:
← mul_one g,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ connectedComponent (g * 1) = {g * 1}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
by
  rw [inf_eq_iInf]
  refine continuousInv_iInf fun b => ?_
  cases b <;> assumption

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
⊢ comap mabs atTop = atBot ⊔ atTop

Tactic:
by
  refine
    le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)
  rintro ⟨a, b⟩ -
  refine ⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩
  rw [mem_preimage, mem_Ici, le_mabs', max_le_iff, ← min_inv_inv', le_min_iff, inv_inv] at hx
  exact hx.imp And.left And.right

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ r < 0

Tactic:
simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]

Goal state after: