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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ (∃ i t, IsPreconnected t ∧ s = mk i '' t) → IsPreconnected s

Tactic:
· rintro ⟨a, t, ht, rfl⟩
    exact ht.image _ continuous_sigmaMk.continuousOn

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

Goal state before:
pp: case inl
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen ∅

pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen univ

Tactic:
exacts [isClopen_empty, isClopen_univ]

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

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

Tactic:
by
  rw [union_eq_iUnion]; exact isLindelof_iUnion fun b => by cases b <;> assumption

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

Goal state before:
pp: case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ x, b ↑x
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✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
⊢ di.extend f b = g b

Tactic:
refine di.extend_eq_of_tendsto fun s hs => mem_map.2 ?_
  suffices ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s from
    hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
  clear hf f
  refine eventually_comap.2 ((hg.eventually hs).mono ?_)
  rintro _ hxs x rfl
  exact hxs

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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
⊢ IsGδ (⋂ i, s i)

Tactic:
choose T hTo hTc hTs using hs

Goal state after:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
s : ι' → Set X
T : ι' → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst✝¹] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
⊢ IsGδ (⋂ i, s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : Nonempty α
⊢ Nonempty (ConnectedComponents α)

Tactic:
ConnectedComponents.nonempty_iff_nonempty

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : Nonempty α
⊢ Nonempty α
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case neg
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 ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
⊢ ⋂ s, ↑s ⊆ b

Tactic:
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
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'
ι : Type u_7
ι' : Type u_8
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpaceProd] (Equiv.sumArrowEquivProdArrow ι ι' X).toFun

Tactic:
dsimp [Equiv.sumArrowEquivProdArrow]

Goal state after:
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'
ι : Type u_7
ι' : Type u_8
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpaceProd] fun f ↦ (f ∘ Sum.inl, f ∘ Sum.inr)
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 Z
W : Type u_5
inst✝ : TopologicalSpace W
f✝ f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
hbij : Bijective ⋯.connectedComponentsMap
⊢ IsHomeomorph ⋯.connectedComponentsMap

Tactic:
exact ⟨hf.continuous.connectedComponentsMap_continuous,
      hf.connectedComponentsMap.isOpenMap_of_injective hbij.injective, hbij⟩

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

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

Tactic:
SetRel.inv,

Goal state after:
α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun x ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun x ↦ (f₂ x, f₃ x)) l (𝓤 α)
⊢ Tendsto (fun x ↦ (f₁ x, f₃ x)) l (𝓤 α)

Tactic:
refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity
  filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩

Goal state after:
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
⊢ f ≤ 𝓝 x

Tactic:
intro s hs
  -- Take an entourage twice smaller than `s`
  rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩
  -- Take a set `t ∈ f`, `t × t ⊆ U`, and a point `y ∈ t` such that `(x, y) ∈ U`
  rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
  apply mem_of_superset t_mem
  -- Given a point `z ∈ t`, we have `(x, y) ∈ U` and `(y, z) ∈ t × t ⊆ U`, hence `z ∈ s`
  exact fun z hz => hU (SetRel.prodMk_mem_comp hxy (ht <| mk_mem_prod hy hz)) rfl

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst✝] (⋃ i ∈ t, {x | (i, x) ∈ s})

Tactic:
exact ht.isClosed_biUnion fun _ _ => hs.preimage <| .prodMk_right _

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 : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)

Tactic:
simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

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 : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ TendstoUniformlyOn F g p s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
  refine forall₂_imp (fun i hi hf => ?_) hf
  rw [eventually_prod_principal_iff] at hf ⊢
  exact hf.mono fun x hx y hy => (((hfg y hy).prod .rfl).mem_open_iff hi.2).mp (hx y hy)

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ s, ball x U = univ

Tactic:
refine iUnion₂_eq_univ_iff.2 fun y => ?_

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ u ≤ id v

Tactic:
id

Goal state after:
α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ u ≤ v
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Tactic:
by
  refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩
  simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]
  exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU

Goal state after:
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 : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' 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

Tactic:
simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]

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 : v ×ˢ w ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
this : ∀ x ∈ K, ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i

Tactic:
choose ind W hW hWU using this

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
ind : (x : α) → x ∈ K → ι
W : (x : α) → x ∈ K → Set (α × α)
hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α
hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i
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 <;> rw [h2]
  exacts [hk.image hf, (hk.image hf).insert 1]

Goal state after:
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 : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p s
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ TendstoLocallyUniformlyOn (fun x ↦ g ∘ F x) (g ∘ f) p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
  refine fun x hx ↦ Tendsto.comp hg (tendsto_inf.mpr ⟨hf x hx, tendsto_principal.mpr ?_⟩)
  filter_upwards [hFs.prod_mk eventually_mem_nhdsWithin] with y hy using ⟨hfs hy.2, hy.1 hy.2⟩

Goal state after:
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)
⊢ TendstoUniformly f (f x) (𝓝 x)

Tactic:
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩

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
⊢ TendstoUniformly f (f x) (𝓝 x)
Module: Mathlib.Algebra.Order.Group.MinMax

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

Tactic:
refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
  · rw [abs_sub_comm a c, abs_sub_comm b d]
    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

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

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

Tactic:
uniformContinuous_pi

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x ↦ toFun x i
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔ TendstoUniformly (⇑toFun ∘ F) (toFun f) p

Tactic:
TendstoUniformly

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ (x : α), (toFun f x, (⇑toFun ∘ F) n x) ∈ u
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:
ext uv

Goal state after:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (S.domRestrict ∘ ⇑UniformFun.toFun) (S.domRestrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β 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₀)
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Tactic:
rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩

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
⊢ f ⁻¹' U ∈ 𝓝[S] x₀
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ (fun x y ↦ ∃ u v, IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
    f g

Tactic:
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
    obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
    exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
uniformContinuous_pi

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (i : ↑(⋃₀ 𝔖)), UniformContinuous fun x ↦ ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖)) x i
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ⇑(toFun 𝔖)

Tactic:
uniformContinuous_pi

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x ↦ (toFun 𝔖) x i
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

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

Tactic:
suffices (· + b) '' (a * ·) '' Ico c d = Ico (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Ico h, image_add_const_Ico]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf,
      ← UniformSpace.comap_comap]

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₁)) ∘ ⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₂)) ∘ ⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β) ≤
    UniformSpace.comap ((fun x ↦ x ∘ ψ₁ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
      UniformSpace.comap ((fun x ↦ x ∘ ψ₂ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ (↑f.symm).comp ↑f = ContinuousMap.id α

Tactic:
by
  rw [← coe_trans, self_trans_symm, coe_refl]

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

Goal state before:
pp: case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x ↦ 0 • x

Tactic:
simp only [zero_smul]

Goal state after:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x ↦ 0
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)

Tactic:
key₂,

Goal state after:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun x ↦ x₀ * y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ (fun x ↦ x * a) '' s ∈ 𝓝 (b * a)

Tactic:
exact smul_mem_nhds_smul (op a) h

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
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ id i) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
id

Goal state after: