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

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x

Tactic:
by
  simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
ι : Type u_1
f : Filter ι
inst✝ : f.IsCountablyGenerated
x : α
u : ι → α
hx : MapClusterPt x f u
⊢ ∃ ψ, Tendsto (u ∘ ψ) atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
by
  grind [exists_seq_comp_tendsto hx]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ u ∈ image π '' V, IsOpen[inst✝] u

pp: case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u

Tactic:
· rintro - ⟨U, U_in_V, rfl⟩
    apply h U (hV.isOpen U_in_V)

Goal state after:
case h_nhds
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ a ∈ s ×ˢ t, 𝓝 a = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y

Tactic:
biSup_prod,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ ⨆ a ∈ s, ⨆ b ∈ t, 𝓝 (a, b) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n

Tactic:
rwa [hs.nhdsSetWithin_prod_eq ht, Filter.mem_prod_iff] at hn

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Type v
inst✝ : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : ∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

Tactic:
simpa using isCompact_univ.inter_iInter_nonempty t htc (by simpa using hst)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ u

Tactic:
rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ v

Tactic:
rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ False

Tactic:
suffices p ∉ closure (S ∩ b) from this <| (h b hb bS) pS

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ p ∉ closure[inst✝] (S ∩ b)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : ↑(irreducibleComponents Y)
⊢ { toFun := fun W ↦ ⟨f ⁻¹' ↑W, ⋯⟩, invFun := fun W ↦ ⟨f '' ↑W, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } W ≤
      { toFun := fun W ↦ ⟨f ⁻¹' ↑W, ⋯⟩, invFun := fun W ↦ ⟨f '' ↑W, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } Z ↔
    W ≤ Z

Tactic:
refine ⟨fun H ↦ ?_, Set.preimage_mono⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
W Z : ↑(irreducibleComponents Y)
H :
  { toFun := fun W ↦ ⟨f ⁻¹' ↑W, ⋯⟩, invFun := fun W ↦ ⟨f '' ↑W, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } W ≤
    { toFun := fun W ↦ ⟨f ⁻¹' ↑W, ⋯⟩, invFun := fun W ↦ ⟨f '' ↑W, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } Z
⊢ W ≤ Z
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (frontier s) t

Tactic:
frontier_eq_closure_inter_closure,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (closure[inst✝¹] s ∩ closure[inst✝¹] sᶜ) t
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ {x}ᶜ ∈ codiscreteWithin s

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
  intro z hz
  use univ \ {x}
  exact ⟨nhdsNE_of_nhdsNE_sdiff_finite univ_mem Finite.of_subsingleton, by aesop⟩

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

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ 𝓝[≠] x = ⊥

Tactic:
← isOpen_singleton_iff_punctured_nhds

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
K : Set X
inst✝ : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K ≤ cofinite ⊓ 𝓟 K

Tactic:
grw [← codiscrete_le_cofinite]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
K : Set X
inst✝ : T1Space X
hK : IsCompact K
⊢ codiscreteWithin K ≤ codiscrete X ⊓ 𝓟 K
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
⊢ IsClopen (s ∩ a)

Tactic:
refine ⟨?_, IsOpen.inter h.2 ha⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
⊢ IsClosed[inst✝] (s ∩ a)
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Tactic:
frontier_eq_closure_inter_closure,

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ closure[inst✝] {b | f b ≤ g b} ∩ closure[inst✝] {b | f b ≤ g b}ᶜ ⊆ {b | f b = g b}
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
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

Tactic:
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: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 ∅)

Tactic:
apply countableInterFilter_principal

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝ : CountableInterFilter l
⊢ CountableInterFilter (𝓟 univ)

Tactic:
apply countableInterFilter_principal

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

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] ((⋃ i, s i) \ s i)

Tactic:
iUnion_sdiff

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (⋃ i_1, s i_1 \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] ((⋃ i, s i) \ s i)

Tactic:
iUnion_sdiff

Goal state after:
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (⋃ i_1, s i_1 \ s i)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inl
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c_count : ∅.Countable
c_cov : s ⊆ ⋃ i ∈ ∅, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

pp: case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
· simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty] at c_cov
    simp only [subset_eq_empty c_cov rfl, empty_subset, exists_const]

Goal state after:
case inr
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
⊢ ∃ f, s ⊆ ⋃ n, U (f n)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
x✝¹ x✝ : X
h : ¬x✝¹ ⤳ x✝
⊢ Disjoint (𝓝ˢ {x✝¹}) (𝓝 x✝)

Tactic:
disjoint_nhdsSet_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
x✝¹ x✝ : X
h : ¬x✝¹ ⤳ x✝
⊢ x✝ ∉ closure[inst✝¹] {x✝¹}
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ IsPreconnected ∅

Tactic:
exact isPreconnected_empty

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝 (SeparationQuotient.mk a))

Tactic:
← disjoint_comap_iff surjective_mk,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (comap SeparationQuotient.mk (𝓝 (SeparationQuotient.mk a)))
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
← disjoint_comap_iff surjective_mk,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (comap mk (𝓝ˢ s)) (comap mk (𝓝ˢ t))
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅

Tactic:
exact isPreconnected_empty

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 (⋃ a, range (Sigma.mk a))

Tactic:
exact isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
← disjoint_comap_iff surjective_mk,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (comap SeparationQuotient.mk (𝓝ˢ t))
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen[inst✝] (f i)
⊢ ⋂ i ∈ I, f i = ⋂₀ (f '' I)

Tactic:
by rw [sInter_image]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

Tactic:
rintro ⟨T, hT, T_count, rfl⟩
    rcases Set.eq_empty_or_nonempty T with rfl | hT
    · exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
    · obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
      exact ⟨f, by simp_all, by simp [hf]⟩

Goal state after:
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 α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ : (i : ι) × ConnectedComponents ↑(U i)
i : ι
x✝ : ConnectedComponents ↑(U i)
x y : { x // x ∈ U i }
hxy : connectedComponent x = connectedComponent y
⊢ (mk ∘ Subtype.val) x = (mk ∘ Subtype.val) y

Tactic:
simp [← heq x.2, ← heq y.2, hxy]

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

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ ∀ (i : Y), {i} ∈ pure i

Tactic:
Filter.mem_pure,

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ ∀ (i : Y), i ∈ {i}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ univ, (f x, F n x) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i

Tactic:
mem_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), True → (f x, F n x) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
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'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))

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 (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformEmbedding g
f : α → β
⊢ IsUniformInducing f ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f

Tactic:
hg.injective.of_comp_iff f

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

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

Tactic:
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
  refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_
  rw [hg.isEmbedding.closure_eq_preimage_closure_image]
  exact preimage_mono (closure_mono <| image_preimage_subset _ _)

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

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f
⊢ HasCompactSupport (f * f')

Tactic:
by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Goal state after:
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, UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
⊢ UniformContinuousOn f s

Tactic:
by
  simp_rw [uniformContinuousOn_iff_restrict, uniformContinuous_def] at h ⊢
  intro u hu
  obtain ⟨v, hv, hvsymm, hvu⟩ := comp_comp_symm_mem_uniformity_sets hu
  obtain ⟨F, hF, hFv⟩ := h v hv
  filter_upwards [hF v hv] with x hx
  exact hvu <| prodMk_mem_comp (prodMk_mem_comp (hFv _ x.1.prop) hx)
      <| hvsymm.symm (f x.2) (F x.2) <| hFv _ x.2.prop

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

Tactic:
by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
    rw [← pure_mul_pure, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.filter

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

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

Tactic:
by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]

Goal state after:
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) '' Ioo c d = Ioo (a * c + b) (a * d + b)

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

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 : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p

Tactic:
tendstoUniformly_congr hF

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
h : TendstoUniformly F' f p
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁴ : Group G✝
inst✝³ : Group H
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → UniformSpace (G i)
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), IsUniformGroup (G i)
⊢ IsUniformGroup ((i : ι) → G i)

Tactic:
by
  rw [Pi.uniformSpace_eq]
  exact isUniformGroup_iInf fun i ↦ .comap (Pi.evalMonoidHom G i)

Goal state after: