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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n ↦ F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
⊢ (∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t) → Tendsto (fun n ↦ F n x) p (𝓝 (f x)) → (f x, F n x) ∈ u

Tactic:
hx

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n ↦ F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
⊢ Tendsto (fun n ↦ F n x) p (𝓝 (f x)) → (f x, F n x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ SetRel.id

Tactic:
simpa [not_imp_not] using @hf x y

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 : β
⊢ x ∈ s → ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
hx

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, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
⊢ ((∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
      ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w) →
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
⊢ ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
⊢ (map f F).TotallyBounded ↔ F.TotallyBounded

Tactic:
refine ⟨fun hs ↦ ?_, fun h ↦ h.map hf.uniformContinuous⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ F.TotallyBounded
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩

Goal state after:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure[inst✝¹] (mulSupport (f ∘ g)))

Tactic:
Function.mulSupport_comp_eq_preimage

Goal state after:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure[inst✝¹] (g ⁻¹' mulSupport f))
Module: Mathlib.Topology.Algebra.Support

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

Tactic:
hx

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

Goal state before:
pp: case refine_2
α : 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
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Continuous[inst✝³.toTopologicalSpace, _] (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))

Tactic:
· exact (continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactorization

Goal state after:
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 s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
⊢ x ∈ s' → ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
⊢ x ∈ t → ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n ↦ F n ∘ g) n y) ∈ u

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n ↦ F n ∘ g) n y) ∈ u
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 ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
F : α → β
hF : ∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s
hFv : ∀ y ∈ s, (f y, F y) ∈ v
x : ↑s × ↑s
⊢ (s.domRestrict F x.1, s.domRestrict F x.2) ∈ v → (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u

Tactic:
hx

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
F : α → β
hF : ∀ r ∈ 𝓤 β, {x | (s.domRestrict F x.1, s.domRestrict F x.2) ∈ r} ∈ 𝓤 ↑s
hFv : ∀ y ∈ s, (f y, F y) ∈ v
x : ↑s × ↑s
hx : (s.domRestrict F x.1, s.domRestrict F x.2) ∈ v
⊢ (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
⊢ x ∈ s → Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst✝¹.toTopologicalSpace, inst✝.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
⊢ {x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
    obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)
    apply
      mem_of_superset
        (symmetrize_mem_uniformity <|
          (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
            symmetrize_mem_uniformity hr)
    rintro ⟨b₁, b₂⟩ h
    by_cases h₁ : b₁ ∈ s; · exact (h.1 h₁).1
    by_cases h₂ : b₂ ∈ s; · exact (h.2 h₂).2
    apply htr
    exact ⟨x, SetRel.symm t <| hst h₁, hst h₂⟩

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

Goal state before:
pp: case hnhds
α : 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
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
⊢ x ∈ k → ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
hx

Goal state after:
case hnhds
α : 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
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: case hnhds
α : 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
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
· rcases comp_symm_of_uniformity hu with ⟨u', u'_mem, u'_symm, hu'⟩
    intro x hx
    obtain ⟨v, hv, w, hw, hvw⟩ :
      ∃ v ∈ 𝓝[s] q, ∃ w ∈ 𝓝[k] x, v ×ˢ w ⊆ f.uncurry ⁻¹' {z | (f q x, z) ∈ u'} :=
        mem_nhdsWithin_prod_iff.1 (hf (q, x) ⟨hq, hx⟩ (mem_nhds_left (f q x) u'_mem))
    refine ⟨w, hw, v, hv, fun p hp y hy ↦ ?_⟩
    have A : (f q x, f p y) ∈ u' := hvw (⟨hp, hy⟩ : (p, y) ∈ v ×ˢ w)
    have B : (f q x, f q y) ∈ u' := hvw (⟨mem_of_mem_nhdsWithin hq hv, hy⟩ : (q, y) ∈ v ×ˢ w)
    exact hu' <| SetRel.prodMk_mem_comp (u'_symm A) B

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V

Tactic:
by
  ext uv
  exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map₂ (fun a b ↦ n (m a b)) f g = map₂ (fun a b ↦ m' (n₁ a) (n₂ b)) f g

Tactic:
h_distrib

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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
⊢ (∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V) →
    x ∈ S → ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
hx

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
⊢ x ∈ S → ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : f ∈ ⋂ i ∈ T, UniformOnFun.gen 𝔗 i V
⊢ f ∈ {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 s V}

Tactic:
simp only [UniformOnFun.gen, Set.mem_iInter, Set.mem_ofPred_eq] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : ∀ i ∈ T, ∀ x ∈ i, ((toFun 𝔗) f.1 x, (toFun 𝔗) f.2 x) ∈ V
⊢ ∀ x ∈ s, ((toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.1) x, (toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.2) x) ∈ V
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : ∀ i ∈ T, ∀ x ∈ i, ((toFun 𝔗) f.1 x, (toFun 𝔗) f.2 x) ∈ V
x : α
⊢ x ∈ s → ((toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.1) x, (toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.2) x) ∈ V

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : ∀ i ∈ T, ∀ x ∈ i, ((toFun 𝔗) f.1 x, (toFun 𝔗) f.2 x) ∈ V
x : α
hx : x ∈ s
⊢ ((toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.1) x, (toFun 𝔖) ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) f.2) x) ∈ V
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
W : Set (α × α)
hW : W ∈ 𝓤 α
hWclosed : IsClosed[instTopologicalSpaceProd] W
hWV : W ⊆ V
x : X
⊢ (∀ (i : ι), (F i x₀, F i x) ∈ W) → x ∈ S → x ∈ f ⁻¹' U

Tactic:
hx

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
W : Set (α × α)
hW : W ∈ 𝓤 α
hWclosed : IsClosed[instTopologicalSpaceProd] W
hWV : W ⊆ V
x : X
hx : ∀ (i : ι), (F i x₀, F i x) ∈ W
⊢ x ∈ S → x ∈ f ⁻¹' U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : IsEmpty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
· infer_instance

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
⊢ x ∈ s → ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) f x) ∈ id U

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
hx : x ∈ s
⊢ ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) f x) ∈ id U
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
ext x
  exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]

Goal state after:
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)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
⊢ UniformFun.uniformSpace (↑S) β =
    ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)

Tactic:
rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
    refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
    simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover

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

Goal state before:
pp: α : Type u_2
inst✝⁶ : TopologicalSpace α
M : Type u_4
β : Type u_5
inst✝⁵ : Ring M
inst✝⁴ : AddCommGroup α
inst✝³ : Module M α
inst✝² : ContinuousConstSMul M α
inst✝¹ : AddGroup β
f : α →+ β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
n : ℤ
hc : IsUnit ↑n
⊢ IsUnit (n • 1)

Tactic:
rwa [zsmul_one n]

Goal state after: