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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝 x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (SeparationQuotient X × SeparationQuotient Y)
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y) ⊓ 𝓟 s) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝[f '' s] f x ≤ map f (𝓝[s] x)

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝[s] x)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝[s] x)

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x ⊓ 𝓟 s)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝[f ⁻¹' {f x}] x ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
nhdsWithin,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
x : X
hx : x ∈ f ⁻¹' s
h : 𝓝 x ⊓ 𝓟 (f ⁻¹' {f x}) ≤ pure x
⊢ 𝓝[f ⁻¹' s] x ≤ pure x
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst✝] u
v : Set X
hv : IsOpen[inst✝] v
x : X
hxs : x ∈ s
hxu : ⟨x, hxs⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty

Tactic:
rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsPreirreducible s
u : Set X
hu : IsOpen[inst✝] u
v : Set X
hv : IsOpen[inst✝] v
x✝ : X
hxs✝ : x✝ ∈ s
hxu✝ : ⟨x✝, hxs✝⟩ ∈ val ⁻¹' u
y : X
hys : y ∈ s
hyv : ⟨y, hys⟩ ∈ val ⁻¹' v
x : X
hxs : x ∈ s
hxu : x ∈ u
hxv : x ∈ v
⊢ (univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' s)

Tactic:
· rw [← compl_compl s, preimage_compl]
      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst✝¹] (connectedComponentIn univ x)

Tactic:
exact isOpen_univ.connectedComponentIn

Goal state after:
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
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)

Goal state after:
α : 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
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, ∀ t ∈ S, (x, y) ∈ t

Tactic:
eventually_countable_ball (p := fun _ _ _ => (_, _) ∈ _) Sct,

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ᶠ (x : α) in l, ∀ i ∈ S, ∀ᶠ (x_1 : β) in m, (x, x_1) ∈ i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ MapsTo f s (Ioi b) ∨ MapsTo f s (Iio b)

Tactic:
simpa [mapsTo_iff_image_subset] using
    (hs.image f hf).subset_or_subset isOpen_Ioi isOpen_Iio (by grind) (by grind)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
y : β
⊢ f ⁻¹' connectedComponent y = ⋃ x ∈ f ⁻¹' connectedComponent y, connectedComponent x

Tactic:
simpa [connectedComponentIn_univ] using
    hf.continuousOn.preimage_connectedComponentIn (F := univ) y

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, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
refine Set.Subset.trans ht.2 ?_

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 ∈ t, (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable ↑I
i : ι
hi : i ∈ I
⊢ IsMeagre (f ↑⟨i, hi⟩)

Tactic:
exact h i hi

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 α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ Disjoint T₁ T₂

Tactic:
refine Disjoint.of_preimage hf ?_

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 v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ Disjoint (f ⁻¹' T₁) (f ⁻¹' T₂)
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
this : DiscreteTopology ↑S
⊢ S.Subsingleton

Tactic:
have : PreconnectedSpace S := isPreconnected_iff_preconnectedSpace.mp hS

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
h : IsDiscrete S
this✝ : DiscreteTopology ↑S
this : PreconnectedSpace ↑S
⊢ S.Subsingleton
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
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ Dense (c n)

Tactic:
rw [dense_iff_closure_eq, subset_antisymm_iff]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ closure[inst✝²] (c n) ⊆ univ ∧ univ ⊆ closure[inst✝²] (c n)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
fin_a : Finset { s // IsClopen s ∧ b ∈ s }
U : Set X := ⋂ i ∈ fin_a, ↑i
ha : connectedComponent a ∩ U = ∅
hU : IsClopen U
⊢ ∃ U V, IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ mk ⁻¹' V = U

Tactic:
exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩

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

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
i : ι
x : X
⊢ x ∈ closure[inst✝²] (g i)

Tactic:
closure_compl,

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
i : ι
x : X
⊢ x ∈ (interior (frontier (f i)))ᶜ
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
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (f '' s)

Tactic:
rwa [← h.1.isOpen_preimage, Set.preimage_image_eq _ h.2]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ ConnectedComponents.mk y = ConnectedComponents.mk x ↔ y ∈ connectedComponent x

Tactic:
ConnectedComponents.coe_eq_coe'

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ connectedComponent x ↔ y ∈ connectedComponent x
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst✝] (s.image t)

Tactic:
simp_rw [SetRel.image, ← exists_prop, Set.ofPred_exists]
  exact isOpen_biUnion fun _ _ => hs.preimage <| .prodMk_right _

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

Goal state before:
pp: case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝ + 1] t ⊆ s

Tactic:
rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩

Goal state after:
case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝ + 1] t ⊆ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ (a, b) ∈ ⋃ p, ⋃ (h : p ∈ s), t p h

Tactic:
simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
x : α
hf : Cauchy (pure x)
⊢ ∃ x_1, pure x ≤ 𝓝 x_1

Tactic:
exact ⟨x, pure_le_nhds x⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
α' : Type u_1
β' : Type u_2
inst✝¹ : UniformSpace α'
inst✝ : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : IsUniformInducing e₁
h₂ : IsUniformInducing e₂
⊢ comap (fun x ↦ ((e₁ x.1.1, e₂ x.1.2), e₁ x.2.1, e₂ x.2.2)) (𝓤 (α' × β')) = 𝓤 (α × β)

Tactic:
simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]

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

Goal state before:
pp: case refine_1
α : 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))
⊢ ∀ (x : α), (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)) (i x) = ff x

Tactic:
simp [ff, hid.inseparable_extend h.uniformContinuous.continuous.continuousAt, sf]

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 : α → β
p : Filter ι
h : ∀ (x : α), ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t
⊢ ∀ x ∈ univ, ∃ t ∈ 𝓝[univ] x, TendstoUniformlyOn F f p t

Tactic:
simpa using h

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ EquicontinuousOn F univ ↔ Equicontinuous F

Tactic:
by
  simp [EquicontinuousOn, Equicontinuous]

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

Goal state before:
pp: α : Type u_2
E : Type u_3
inst✝² : CommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f g : α → E
m : E
x : Filter α
hf : Tendsto f x (𝓝 m)
hfg : Tendsto (g / f) x (𝓝 1)
⊢ Tendsto g x (𝓝 m)

Tactic:
simpa using Tendsto.mul hf hfg

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ g) = map₂ m f g

Tactic:
map₂,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p ↦ m p.1 p.2) (f ×ˢ g) = (map (uncurry m) (f ×ˢ g)).copy {s | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} ⋯
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]

Goal state after:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ 𝔖 = ⨅ b, bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x ↦ x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]

Tactic:
simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
H : ⋃ i, S i = Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] ((S i).domRestrict (Set.liftCover S (fun i ↦ ⇑(φ i)) hφ H))

Tactic:
simpa +unfoldPartialApp only [Set.domRestrict, Set.liftCover_coe]
      using map_continuous (φ i)

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Ioi c
⊢ b * f x✝¹ ∈ Ioi (b * c)

Tactic:
rw [Set.mem_Ioi] at *; gcongr

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Ioi c
⊢ f x✝¹ * b ∈ Ioi (c * b)

Tactic:
rw [Set.mem_Ioi] at *; gcongr

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩

Goal state after:
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ↑𝒰 ≤ 𝓝 (x, z)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
refine continuousMul_iInf fun b => ?_

Goal state after:
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : ∀ i ∈ cons a s ha, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x

Tactic:
simp_rw [Finset.mem_cons, forall_eq_or_imp] at h

Goal state after:
case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ K ∈ 𝓝 ((y * x⁻¹)⁻¹ • y)

Tactic:
simpa using h

Goal state after: