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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ s ⊆ connectedComponentIn F x

Tactic:
by
  have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
  have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs
  have := this.subset_connectedComponent h2xs
  rw [connectedComponentIn_eq_image (hsF hxs)]
  refine Subset.trans ?_ (image_mono this)
  rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
⊢ ∀ (u v : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
intro u

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u : Set α
⊢ ∀ (v : Set α), IsClosed[inst✝¹] u → IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ ∀ (i' : Set X), IsLindelof i' → ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Tactic:
intro t ht

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set X
ht : IsLindelof t
⊢ ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ
Module: Mathlib.Topology.GDelta.Basic

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

Tactic:
by simp [hf]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

Tactic:
intro u

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
⊢ u ∈ image f '' T → IsNowhereDense u
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (f : ℕ → Set Y), (∀ (n : ℕ), IsOpen[inst✝] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)

Tactic:
intro u

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
u : ℕ → Set Y
⊢ (∀ (n : ℕ), IsOpen[inst✝] (u n)) → (∀ (n : ℕ), Dense (u n)) → Dense (⋂ n, u n)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
    rw [union_comm] at H
    have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
    by_cases hxu : x ∈ u <;> [left; right]
    -- The x ∈ u case.
    · suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
        from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
      · apply Subset.trans _ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩
    -- If x ∉ u, we get x ∈ v since x ∈ u ∪ v. The rest is then like the x ∈ u case.
    · have h1 : x ∈ v :=
        (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
      suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab
      · refine Subset.trans ?_ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

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

Tactic:
have := h.symm.continuous.continuousOn.image_connectedComponentIn_subset (mem_image_of_mem h hx)

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 : ⇑h.symm '' connectedComponentIn (⇑h '' s) (h x) ⊆ connectedComponentIn (⇑h.symm '' ⇑h '' s) (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
⊢ ∀ (i : S ⊕ T), Continuous[instTopologicalSpaceProd, inst✝ i] fun a ↦ (Equiv.sumPiEquivProdPi A).invFun a i

Tactic:
rintro (s | t) <;> dsimp

Goal state after:
case inl
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inl s)] fun a ↦ a.1 s

case inr
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst✝ : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst✝ (Sum.inr t)] fun a ↦ a.2 t
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u ↦ ↑u⁻¹) x

Tactic:
intro u

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
⊢ ContinuousAt (fun u ↦ ↑u⁻¹) u
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ Continuous[inst✝³, inst✝²] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst✝³, inst✝²] f ∧ Bijective f

Tactic:
refine and_congr_right fun hf ↦ ?_

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
⊢ u₁ = u₂

Tactic:
by ext; exact h _

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x ∈ t, ↑l ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x)

Tactic:
exact fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n ↦ F n x) p (𝓝 (f x))

Tactic:
simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
  exact forall₂_congr fun u _ => by simp [preimage]

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
⊢ ∃ x ∈ univ, f ≤ 𝓝 x

Tactic:
rcases CompleteSpace.complete hf with ⟨x, hx⟩

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompleteSpace α
f : Filter α
hf : Cauchy f
x✝ : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ x ∈ univ, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
⊢ UniformCauchySeqOnFilter F p p'

Tactic:
intro u

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
⊢ u ∈ 𝓤 β → ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
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
⊢ TendstoUniformlyOnFilter F f p p'

Tactic:
intro u

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 (β × β)
⊢ u ∈ 𝓤 β → ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ 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
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 SetRel.id

Tactic:
calc
    comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
    _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
    _ ≤ 𝓟 SetRel.id := principal_mono.2 ?_

Goal state after:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
⊢ Prod.map f f ⁻¹' s ⊆ SetRel.id
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'
⊢ UniformCauchySeqOn (fun i ↦ Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

Tactic:
intro u

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 ((β × β') × β × β')
⊢ u ∈ 𝓤 (β × β') →
    ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
      ∀ x ∈ s ×ˢ s', ((fun i ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun i ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy (map m x) → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
hm.cauchy_map_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p ↦ (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)

Tactic:
intro u

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
⊢ u ∈ 𝓤 β → u ∈ map (fun p ↦ (F p.1 x, F p.2 x)) (p ×ˢ p)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
⊢ ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ x) atTop (𝓤 β)

Tactic:
intro u

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
u : ℕ → ι × α
⊢ Tendsto u atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ ∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id i) t ∈ F

Tactic:
intro t ht

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
⊢ ∃ t_1, t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
⊢ IsCompact (range f)

Tactic:
rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2

Goal state after:
case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = f '' K
⊢ IsCompact (range f)

case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
K : Set α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝², inst✝] f
hk : IsCompact K
h'f : mulSupport f ⊆ K
h2 : range f = insert 1 (f '' K)
⊢ IsCompact (range f)
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ Filter.comap (fun x ↦ (const ι x.1, const ι x.2)) (𝓤 (ι → X)) = ⨅ i, 𝓤 X

Tactic:
Pi.uniformity,

Goal state after:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
⊢ Filter.comap (fun x ↦ (const ι x.1, const ι x.2)) (⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 X)) = ⨅ i, 𝓤 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 s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoLocallyUniformlyOn F f p s'

Tactic:
intro u

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 (β × β)
⊢ u ∈ 𝓤 β → ∀ 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
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p t

Tactic:
intro u

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 (β × β)
⊢ u ∈ 𝓤 β → ∀ 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
⊢ ∀ r ∈ 𝓤 β, {x | (s.domRestrict f x.1, s.domRestrict f x.2) ∈ r} ∈ 𝓤 ↑s

Tactic:
intro u

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 (β × β)
⊢ u ∈ 𝓤 β → {x | (s.domRestrict f x.1, s.domRestrict f x.2) ∈ u} ∈ 𝓤 ↑s
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
have : UniformContinuousOn ↿f (K ×ˢ univ) :=
    IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
      (h.mono <| prod_mono hKU Subset.rfl)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ Tendsto (fun x ↦ (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f))) (𝓤 (α →ᵤ β)) (𝓤 (γ →ᵤ β))

Tactic:
(UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 (α → β)) = 𝓤 (α →ᵤ[{s | s.Finite}] β)

Tactic:
Pi.uniformity,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (⨅ i, comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 β)) =
    𝓤 (α →ᵤ[{s | s.Finite}] β)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
uniformEquicontinuous_iff_uniformContinuous,

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ UniformContinuous (⇑ofFun ∘ swap F) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Order.Filter.NAry

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

Tactic:
by
  rw [map₂_swap, map₂_map_left, map₂_swap]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
uniformEquicontinuous_iff_uniformContinuous,

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformContinuous (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
uniformEquicontinuous_iff_uniformContinuous,

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformContinuous (⇑ofFun ∘ swap F) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
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✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun x2 ↦ 1 • x2) f = f

Tactic:
one_smul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun x2 ↦ x2) f = f