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

Goal state before:
pp: case refine_1
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)
U V : Set Y
Uo : IsOpen[inst✝¹] U
Vo : IsOpen[inst✝¹] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ (f ⁻¹' V)ᶜ ∈ 𝓝 x

Tactic:
filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx

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
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)

Tactic:
refine ⟨fun S hSc hS => ?_⟩
  choose s hs t ht hst using hS
  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
  refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
  rw [hst i hi]
  apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
⊢ False

Tactic:
have yu : y ∉ u := (h' ys).elim id (absurd yv)

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
⊢ False
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
· exact (h x).anti (hs.subset_connectedComponent x_in)

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 : α → β
⊢ ∀ (x : ConnectedComponents α), connectedComponent x = {x}

Tactic:
refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
x : α
⊢ connectedComponent (mk x) = {mk x}
Module: Mathlib.Topology.GDelta.Basic

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

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

Tactic:
· rw [← compl_compl_image S]; exact hc.image _

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
⊢ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x

Tactic:
ext y

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ g ×ˢ f ↔ R.inv ∈ g ×ˢ f

Tactic:
R.inv_eq_self

Goal state after:
α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ g ×ˢ f ↔ R ∈ g ×ˢ f
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ Cauchy l ↔ Cauchy (map f l)

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
  rfl

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

Goal state before:
pp: β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x : β
⊢ ball x V = {y | (y, x) ∈ V}

Tactic:
ext y

Goal state after:
β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
⊢ Tendsto Prod.swap (𝓟 SetRel.id) (𝓟 SetRel.id)

Tactic:
simp [Tendsto, SetRel.id]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : (𝓤 α).IsCountablyGenerated
inst✝¹ : UniformSpace β
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (𝓤 (α × β)).IsCountablyGenerated

Tactic:
rw [uniformity_prod]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : (𝓤 α).IsCountablyGenerated
inst✝¹ : UniformSpace β
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β)).IsCountablyGenerated
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ 𝓤 (α × β)

Tactic:
rw [uniformity_prod]

Goal state after:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case inl.inl
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs : s ∈ map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p ↦ (inl p.1, inl p.2)) ⁻¹' s
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p ↦ (inr p.1, inr p.2)) ⁻¹' s
a b : α
hab : (a, b) ∈ tα
c : α
hbc : (b, c) ∈ tα
⊢ (inl (a, b).1, inl (b, c).2) ∈ s

pp: case inr.inr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs : s ∈ map (fun p ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p ↦ (inr p.1, inr p.2)) (𝓤 β)
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun p ↦ (inl p.1, inl p.2)) ⁻¹' s
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun p ↦ (inr p.1, inr p.2)) ⁻¹' s
a b : β
hab : (a, b) ∈ tβ
c : β
hbc : (b, c) ∈ tβ
⊢ (inr (a, b).1, inr (b, c).2) ∈ s

Tactic:
exacts [@Htα (_, _) ⟨b, hab, hbc⟩, @Htβ (_, _) ⟨b, hab, hbc⟩]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝¹ : CompleteSpace α
f : Filter α
inst✝ : f.NeBot
hf : f.TotallyBounded
⊢ ∃ x, ClusterPt x f

Tactic:
let m := Ultrafilter.of f
  have hmf : m ≤ f := Ultrafilter.of_le f
  have hm := m.cauchy_of_totallyBounded' (hf.mono hmf)
  obtain ⟨x, hx⟩ := CompleteSpace.complete hm
  rw [le_nhds_iff_adhp_of_cauchy hm] at hx
  exact ⟨x, hx.mono hmf⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
U : (x : α) → x ∈ K → Set α
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
V : Set (α × α)
V_uni : V ∈ 𝓤 α
hV : ∀ x ∈ K, ∃ i, ball x V ⊆ interior (U ↑i ⋯)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U ↑y ⋯

Tactic:
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
V : Set (α × α)
V_uni : V ∈ 𝓤 α
hV : ∀ x ∈ K, ∃ i, ball x V ⊆ interior (U i)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y

Tactic:
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

Goal state after:
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

Tactic:
exact SeparationQuotient.isUniformInducing_mk

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
rw [← nhdsWithin_univ] at hunif hg

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))
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✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf : Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ Tendsto (fun y ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Goal state after:
α : 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✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 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, (f x.2, G x.1 x.2) ∈ id i
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 : Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ Tendsto (fun y ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

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

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

Tactic:
by
  -- By definition of the product uniform structure, this is just `uniform_continuous_eval`.
  rw [uniformContinuous_pi]
  intro x
  exact uniformContinuous_eval β x

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ) = uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)

Tactic:
UniformFun.comap_eq,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : UniformSpace.comap (fun x ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓ uniformSpace α (β × γ) = uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)

Tactic:
rcases h_cover with ⟨I, I_finite, I_cover⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i ∈ 𝔖,
      UniformSpace.comap (fun x ↦ f ∘ x)
        (UniformSpace.comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑i) β))

Tactic:
UniformFun.comap_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ s ∈ 𝔖,
      UniformSpace.comap (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformSpace.comap (fun x ↦ f ∘ x) (UniformFun.uniformSpace (↑s) β)) =
    ⨅ i ∈ 𝔖,
      UniformSpace.comap (fun x ↦ f ∘ x)
        (UniformSpace.comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑i) β))
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
by
  -- This is a direct consequence of `UniformOnFun.comap_eq`
  rw [uniformContinuous_iff_le_comap]
  exact (UniformOnFun.mono (uniformContinuous_iff_le_comap.mp hf)
    subset_rfl).trans_eq UniformOnFun.comap_eq

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
⊢ False

Tactic:
have : x ∈ t * (closure {1} : Set G) := by
    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
    simp only [mem_compl_iff, not_not] at H
    exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure[inst✝²] {1}
⊢ False
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Tendsto (fun x ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
⊢ ∃ x, ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
exact hf.eventually_mem K_mem |>.curry.exists

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝⁷ : Monoid A
inst✝⁶ : Monoid B
inst✝⁵ : Monoid C
inst✝⁴ : Monoid D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
f g : A →ₜ* B
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformContinuous ⇑(Equiv.inv G)

Tactic:
apply uniformContinuous_iff_le_comap.2

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ IsTopologicalGroup.rightUniformSpace G ≤ UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ UniformContinuous ⇑(Equiv.inv G)

Tactic:
apply uniformContinuous_iff_le_comap.2

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤ UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.rightUniformSpace G)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ G ≃ᵤ G

Tactic:
by
  have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G)
      (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff_le_comap.2
    rw [← comap_inv_leftUniformSpace]
  have B : @UniformContinuous G G (IsTopologicalGroup.leftUniformSpace G)
      (IsTopologicalGroup.rightUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff_le_comap.2
    rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]
    simp
  exact @UniformEquiv.mk G G (IsTopologicalGroup.rightUniformSpace G)
    (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) A B

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun a ↦ f (g a))

Tactic:
BddAbove,

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬(upperBounds (range fun a ↦ f (g a))).Nonempty
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j : ℕ
⊢ ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
rcases hx i with ⟨M, hM⟩

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
⊢ ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
this : ∀ x ∈ t, ∃ y > x, s ∩ Ioo x y = ∅
⊢ t.Countable

Tactic:
choose! y hy h'y using this

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
⊢ t.Countable
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

Tactic:
apply min_le_right

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

Tactic:
apply min_le_right

Goal state after: