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

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
filter_upwards [eventually_nhdsWithin_iff.1 (disjoint_principal_right.1 (hs x h₁x))]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
⊢ ∀ (a : X), (a ∈ {x}ᶜ → a ∉ U \ s) → a ∈ (U \ s)ᶜ
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 : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
refine ⟨ht.1.preimage_of_isPreirreducible_fiber f hf₂ hf₃ h, fun u hu htu ↦ image_subset_iff.mp
    (subset_closure.trans (ht.2 (hu.image f hf₁.continuousOn).closure ?_))⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (f '' u)
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 : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False

Tactic:
have : g x ∈ Uf ∩ Ug := 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 : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
this : g x ∈ Uf ∩ Ug
⊢ False
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)

Tactic:
exact fun F hF x _ => hF.connectedComponentIn

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
⊢ s = ∅ ∨ s = univ → IsClopen s

Tactic:
rintro (rfl | rfl); exacts [isClopen_empty, isClopen_univ]

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

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed[inst✝] (u ∩ s) → IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)

Tactic:
· rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

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

Goal state before:
pp: 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 ⊆ e ∩ U
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ e ∩ V
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ SeparatedNhds s t

Tactic:
inter_comm e

Goal state after:
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)
⊢ SeparatedNhds s t
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ x ∈ V₁

Tactic:
rwa [← di.extend_eq_of_tendsto hc] at hc

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure[inst✝] (e '' {x | p x})
⊢ ⟨x, hx⟩ ∈ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) ↔ ⟨x, hx⟩ ∈ univ

Tactic:
image_eq_range

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure[inst✝] (e '' {x | p x})
hx : x ∈ closure[inst✝] (range fun x ↦ e ↑x)
⊢ ⟨x, hx✝⟩ ∈ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) ↔ ⟨x, hx✝⟩ ∈ univ
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
s : Set Y
hf : Continuous[inst✝¹, inst✝] f
hs : IsGδ s
U : ℕ → Set Y
hU1 : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hU2 : s = ⋂ n, U n
⊢ IsGδ (f ⁻¹' s)

Tactic:
simp_all only [preimage_iInter]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst✝¹, inst✝] f
U : ℕ → Set Y
hs : IsGδ (⋂ n, U n)
hU1 : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hU2 : s = ⋂ n, U n
⊢ IsGδ (⋂ i, f ⁻¹' U i)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ IsMeagre (s ∪ t)

Tactic:
by
  rw [IsMeagre, compl_union]
  exact inter_mem hs ht

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

Tactic:
preimage_subtype_coe_eq_compl hsuv H

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' v)ᶜ
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
⊢ s ∈ f

Tactic:
rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, (fun x ↦ t ○ x)^[n] t ⊆ s

Tactic:
suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
  induction n generalizing s with
  | zero => simpa
  | succ _ ihn =>
    rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
    refine (ihn htU).mono fun U hU => ?_
    rw [Function.iterate_succ_apply']
    have := isRefl_of_mem_uniformity htU
    exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)

Tactic:
let _ : TopologicalSpace α := ⊥

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x✝ : TopologicalSpace α := ⊥
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)
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 ∈ 𝓤 α
A : ∀ x ∈ s, ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
⊢ ∃ t, IsOpen[inst✝] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Tactic:
choose! t t_open xt ht using A

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 ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
⊢ ∃ t, IsOpen[inst✝] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case right
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : SetRel.preimage t (f '' u) ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F

Tactic:
simp_rw [SetRel.preimage, exists_mem_image] at h

Goal state after:
case right
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : {a | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst✝ : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop univ

Tactic:
exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : (x : α) → x ∈ K → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ⊆ U ↑y ⋯) → ∀ x ∈ K, ∃ y, ball x s ⊆ U ↑y ⋯

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ⊆ U y) → ∀ x ∈ K, ∃ y, ball x s ⊆ U y

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (Equiv.ofInjective f ⋯).invFun

Tactic:
hf.isUniformInducing.uniformContinuous_iff,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (f ∘ (Equiv.ofInjective f ⋯).invFun)
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, (∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s) ∧ ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ {x | (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u} ∈ 𝓤 ↑s

Tactic:
obtain ⟨v, hv, hvsymm, hvu⟩ := comp_comp_symm_mem_uniformity_sets hu

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ F, (∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s) ∧ ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
⊢ {x | (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u} ∈ 𝓤 ↑s
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u

Tactic:
intro t t' ⟨v, v_mem, hv⟩ ⟨v', v'_mem, hv'⟩

Goal state after:
case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
Module: Mathlib.Topology.UniformSpace.HeineCantor

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

Tactic:
rw [equicontinuous_iff_continuous] at h
  rw [uniformEquicontinuous_iff_uniformContinuous]
  exact CompactSpace.uniformContinuous_of_continuous h

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
rintro h x hx u hu
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx
    exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
⊢ ∃ z ∈ 𝔖, (fun x1 x2 ↦ x1 ⊆ x2) s₁ z ∧ (fun x1 x2 ↦ x1 ⊆ x2) s₂ z

Tactic:
by
    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
⊢ map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h)

Tactic:
by
  rintro s ⟨t₁, ⟨u₁, hu₁, v, hv, ht₁⟩, t₂, ⟨u₂, hu₂, w, hw, ht₂⟩, hs⟩
  refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
  refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
  · exact (image2_subset_right inter_subset_left).trans ht₁
  · exact (image2_subset_right inter_subset_right).trans ht₂

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * b * y ≤ a * c
⊢ b * y ≤ c

Tactic:
mul_assoc,

Goal state after:
case mpr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c y : α
hy : 1 ≤ y
habx : a * b ≤ a * b * y
hxac : a * (b * y) ≤ a * c
⊢ b * y ≤ c
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d

Tactic:
mul_assoc,

Goal state after:
case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
x✝ : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * (c * y) ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g

Tactic:
refine (map_map₂_distrib_left fun _ _ => ?_).symm

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
x✝¹ : β
x✝ : γ
⊢ a • x✝¹ • x✝ = (a • x✝¹) • x✝
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
hf : Continuous[inst✝¹, inst✝] f
⊢ mkD f g = { toFun := f, continuous_toFun := hf }

Tactic:
simp only [mkD, hf, ↓reduceDIte]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
hf : ¬Continuous[inst✝¹, inst✝] f
⊢ mkD f g = g

Tactic:
simp only [mkD, hf, ↓reduceDIte]

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

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

pp: case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
· left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]

Goal state after:
case h.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb✝ : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
⊢ uniformSpace α β 𝔖 =
    ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

Tactic:
set ψ : Π S : Set α, Π i : ι, (φ i) ⁻¹' S → S := fun S i ↦ S.restrictPreimage (φ i)

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
⊢ uniformSpace α β 𝔖 =
    ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SMul M α
inst✝³ : ContinuousConstSMul M α
inst✝² : TopologicalSpace β
g : β → α
b : β
s : Set β
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
c : M
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ MulOpposite.op c • x

Tactic:
simpa only [op_smul_eq_smul] using continuous_const_smul c

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

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 ↦ f x * x_1) (map (⇑f) (𝓝 1)) ≤ map (fun x_1 ↦ f (x * x_1)) (𝓝 1)

Tactic:
simp [Function.comp_def]

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
⊢ Tendsto ?m.78 (𝓝 (1, 1)) (𝓝 1)

Tactic:
simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G)

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

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

Tactic:
rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]

Goal state after: