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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsPreirreducible S ↔ S.Subsingleton

Tactic:
by
  simp [isPreirreducible_iff_forall_mem_subset_closure_singleton, Set.Subsingleton, eq_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
this : Finite ↑s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, U ∩ s = {x}

Tactic:
by
  simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hs hx

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

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Tactic:
· intro hd hbot
    rw [hbot.atBot_eq, disjoint_principal_right] at hd
    exact mem_of_mem_nhds hd le_rfl

Goal state after:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[≠] a

Tactic:
← nhdsLT_sup_nhdsGT,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[<] a ⊔ 𝓝[>] a
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t
  have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
      ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
  refine isPreconnected_of_forall_pair ?_
  intro x hx y hy
  obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
  obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
  obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
  exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
    mem_biUnion hjp hyj, hp⟩

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

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
exact hmono sᶜ ht tᶜ hsub

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ P x y

Tactic:
let Q : s → s → Prop := fun a b ↦ P a b

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := fun a b ↦ P ↑a ↑b
⊢ P x y
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ ⋃ i ∈ r, interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
apply iUnion₂_subset

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
⊢ ∀ i ∈ r, interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case sUnion
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
S : Set (Set X)
a✝ : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, a ∈ s → Disjoint (𝓝ˢ sᶜ) (𝓝 a)
ha : a ∈ ⋃₀ S
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)

Tactic:
obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ B, x ∈ t ∧ closure[inst✝¹] t ⊆ s

Tactic:
simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
intro u v hu hv hs huv
    rw [isPreconnected_closed_iff] at h
    specialize h u v hu hv hs
    contrapose! huv
    simp only [not_subset] at huv
    rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
    have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
    have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
    exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
⊢ ContinuousOn (Prod.mk a₁) t

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f
⊢ False

Tactic:
rw [← compl_iUnion₂] at uninf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Set ↑s
ht : t.Countable
h : s ⊆ ⋃ i ∈ t, U i
uinf : ⋃ i ∈ t, U i ∈ f.sets
uninf : (⋃ i ∈ t, U i)ᶜ ∈ f
⊢ False
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T4Space X
s✝ : Set X
a✝ : X
hs : IsClosed[inst✝¹] s✝
hxs : a✝ ∉ s✝
⊢ Disjoint (𝓝ˢ s✝) (𝓝 a✝)

Tactic:
simpa only [nhdsSet_singleton] using (normal_separation hs isClosed_singleton
    (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet

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 ⊆ ⋃ x, b ↑x

Tactic:
exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsSigmaCompact s
⊢ IsLindelof s

Tactic:
by
  rw [IsSigmaCompact] at hs
  rcases hs with ⟨K, ⟨hc, huniv⟩⟩
  rw [← huniv]
  have hl : ∀ n, IsLindelof (K n) := fun n ↦ IsCompact.isLindelof (hc n)
  exact isLindelof_iUnion hl

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof univ

Tactic:
by rw [hf.isInducing.isLindelof_iff, image_univ]; exact hf.isClosed_range.isLindelof

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LindelofSpace (X i)
⊢ IsLindelof univ

Tactic:
rw [Sigma.univ]

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LindelofSpace (X i)
⊢ IsLindelof (⋃ a, range (Sigma.mk a))
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 α
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TotallyDisconnectedSpace Y
inst✝ : ConnectedSpace X
y : Y
⊢ Continuous[inst✝³, inst✝²] fun x ↦ y

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set ↑s
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst✝¹] (V n)) ∧ s = ⋂ n, V n
g : ℕ → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst✝¹] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val ⁻¹' g n = f n
n : ℕ
⊢ s ⊆ V n

Tactic:
simp [hV.2, iInter_subset]

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

Goal state before:
pp: 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

Tactic:
fun_prop

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

Goal state before:
pp: 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

Tactic:
fun_prop

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] fun f ↦ (f ∘ Sum.inl, f ∘ Sum.inr)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
a : β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1, a)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
a : β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (a, p.2)

Tactic:
fun_prop

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 ι
⊢ ∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a

Tactic:
simp_rw [eventually_prod_principal_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, True
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s ↦ g (ball x s)

Tactic:
simp_rw [ball, Function.comp_def]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s ↦ g {y | (y, x) ∈ s}

Tactic:
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
  simp_rw [Function.comp_def, preimage]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto Prod.swap (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β)) (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
simp only [tendsto_comap_iff]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto ((fun p ↦ (f p.1, f p.2)) ∘ Prod.swap) (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β)) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' f (mk a) = f a

Tactic:
lift',

Goal state after:
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ (if hc : UniformContinuous f then lift f ⋯ else fun x ↦ f ⋯.some) (mk a) = f a
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
lift',

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (if hc : UniformContinuous f then lift f ⋯ else fun x ↦ f ⋯.some)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
lift',

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (if hc : UniformContinuous f then lift f ⋯ else fun x ↦ f ⋯.some)
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
this : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
rcases this with ⟨U, hU, hUAB⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst✝.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
L : ∀ u ∈ 𝓤 β, ∃ F, Continuous[inst✝¹, inst✝.toTopologicalSpace] F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
simpa [continuousOn_univ] using L

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 : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformly (fun n ↦ F n ∘ g) (f ∘ g) p

Tactic:
by
  rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
  rw [← continuousOn_univ] at cg
  exact h.comp _ (mapsTo_univ _ _) cg

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

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

Goal state before:
pp: G✝ : Type u_1
α : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace X
G : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1 * p.2⁻¹

Tactic:
exact continuous_mul.comp₂ continuous_fst <| continuous_inv.comp continuous_snd

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ a * x) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x * a) ⁻¹' Ioc b c = Ioc (b / a) (c / a)

Tactic:
simp [← Ioi_inter_Iic]

Goal state after:
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 α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f

Tactic:
by simp only [← Filter.map_smul, map_map, Function.comp_def, ← mul_smul]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
α : Type u_7
inst✝⁹ : Monoid N
inst✝⁸ : SMul M N
inst✝⁷ : MulAction N α
inst✝⁶ : SMul M α
inst✝⁵ : IsScalarTower M N α
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousSMul M N
inst✝ : ContinuousSMul N α
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ (p.1 • 1) • p.2

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁸ : FunLike F α β
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : Module R α
inst✝³ : Module R β
inst✝² : TopologicalSpace R
inst✝¹ : LinearMapClass F R α β
tβ : TopologicalSpace β
inst✝ : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] fun x ↦ x.1 • f x.2

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : MulAction M X
inst✝¹ : ContinuousSMul M X
inst✝ : DiscreteTopology X
x : X
⊢ Continuous[inst✝⁵, inst✝⁴] fun g ↦ g • x

Tactic:
fun_prop

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
y x : X
U : Set M := {m' | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
⊢ Continuous[inst✝⁵, inst✝⁵] fun m' ↦ m' * m⁻¹

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.domRestrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 ↦ ↑(F' i i_1)) = F
f' : α → ↑s
hf' : (fun i ↦ ↑(f' i)) = f
comp_tendstoUniformly :
  (∀ (i : ι) (x : α), ↑(F' i x) ∈ s) →
    (∀ (x : α), ↑(f' x) ∈ s) →
      UniformContinuousOn g s →
        TendstoUniformly (fun i i_1 ↦ ↑(F' i i_1)) (fun i ↦ ↑(f' i)) p →
          TendstoUniformly (fun i x ↦ g ↑(F' i x)) (fun x ↦ g ↑(f' x)) p
h : Tendsto (fun q ↦ (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly F' f' p

Tactic:
rwa [← tendstoUniformly_iff_tendsto] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ᶠ (i : ι) in p, ∀ (x : ↑t), t.domRestrict (F i) x ∈ s

Tactic:
simpa using hF

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : SeparatelyContinuousMul M
a✝ : ULift.{u, u_3} M
⊢ Continuous[ULift.topologicalSpace, inst✝²] fun x ↦ a✝.down * x.down

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : SeparatelyContinuousMul M
a✝ : ULift.{u, u_3} M
⊢ Continuous[ULift.topologicalSpace, inst✝²] fun x ↦ x.down * a✝.down

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
⊢ Continuous[instTopologicalSpaceProd, inst✝²] fun p ↦ p.1.down * p.2.down

Tactic:
fun_prop

Goal state after: