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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ n, compactCovering X n = univ

Tactic:
by
  rw [compactCovering, iUnion_accumulate]
  exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
htn : ∀ (i : ι), (t i).Nonempty
i j : ι
hji₀ : t i₀ ⊇ t j
hji : t i ⊇ t j
⊢ (t i₀ ∩ t i).Nonempty

Tactic:
exact (htn j).mono (subset_inter hji₀ hji)

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

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

Tactic:
compl_iInter₂

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ i ∈ t, U i
⊢ s ⊆ ⋃ i ∈ t, (U i)ᶜᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
intro F hsF

Goal state after:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
⊢ ∃ x ∈ s, ↑F ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set ↑P
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, ↑⟨↑i, ⋯⟩
⊢ s ⊆ ⋃₀ ((fun x ↦ ↑x) '' J)

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure[inst✝] tᶜ = s' ∩ closure[inst✝] tᶜ

Tactic:
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
  rwa [frontier_compl, eq_comm]

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

Goal state before:
pp: case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
exact fun i ↦ H.image <| continuous_apply i

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
U : Finset (Set X)
hu : ∀ u ∈ U, IsOpen[inst✝] u
hU : ∀ u ∈ U, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑U).Nonempty

Tactic:
induction U using Finset.induction_on with

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

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
⊢ V'ᶜᶜ.Nonempty

Tactic:
· simp only [compl_compl, V'ne]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
⊢ Z ∈ S

Tactic:
by
  obtain ⟨W, hWS, hZW⟩ := isIrreducible_iff_sUnion_isClosed.mp hZ.1 hS.toFinset
    (fun W hW ↦ isClosed_of_mem_irreducibleComponents W (hSα (hS.mem_toFinset.mp hW)))
    (hS.coe_toFinset.symm ▸ hZS)
  rw [hS.mem_toFinset] at hWS
  rwa [Set.Subset.antisymm hZW (hZ.2 (hSα hWS).1 hZW)]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
by
  refine le_antisymm (nhdsSet_inter_le _ _) ?_
  simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]
  refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_
  rcases eq_or_ne x y with (rfl | hne)
  · exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le
  · exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
ht : IsPreirreducible t
hU : U.Nonempty
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
⊢ IsIrreducible S

Tactic:
by
  obtain ⟨z, hz⟩ := hU
  replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩
  refine ⟨⟨z, h₁ hz⟩, ?_⟩
  rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
  obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) := by
    refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
    · simp [*]
    · intro U H
      simp only [Finset.mem_insert, Finset.mem_singleton] at H
      rcases H with (rfl | rfl | rfl)
      exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
  replace hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
  exact ⟨x, h₁ hx'.1, hx'.2⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m

Tactic:
by
  rw [← reflTransGen_swap]
  exact reflTransGen_of_succ_of_le (swap r) h hmn

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
z : X
hz : z ∈ t
⊢ univ \ t ∩ (t \ s) = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ univ \ {x} ∩ (s \ {x}ᶜ) = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t✝ : Set X
h : t✝.Finite
τ : X
t : Set X
hτ : τ ∉ t
h₁t : t.Finite
h₂t : tᶜ ∈ codiscreteWithin s
⊢ (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous[inst✝, _] U.boolIndicator ↔ IsClopen U

Tactic:
by
  rw [continuous_bool_rng true, preimage_boolIndicator_true]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ f x ∈ interior s

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ s ∈ 𝓝 (f x)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X = cocompact X

Tactic:
by
  refine le_antisymm ?_ cocompact_le_coclosedCompact
  rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]
  exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite →
    LocallyConnectedSpace ((i : ι) → X i)

Tactic:
rintro (he | ⟨hloc, hfin⟩)
    · exact ⟨he.elim⟩
    · exact locallyConnectedSpace_of_finite_not_preconnectedSpace hfin

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s (succ k) ∩ s k).Nonempty

Tactic:
by rw [inter_comm]; exact h3 hj hi hk

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ f ⁻¹' u ∩ s ∪ f ⁻¹' v ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
u'_eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∩ s ∪ f ⁻¹' v ∩ s
⊢ s ⊆ u' ∪ v'
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
⊢ s.Nonempty ∧ sᶜ.Nonempty

Tactic:
simpa [nonempty_iff_ne_empty] using h

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 : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
U : Finset (Set α)
hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ U, IsOpen[inst✝] u
hsU : s ⊆ ⋃₀ ↑U
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∃ u ∈ U, s ⊆ u

Tactic:
induction U using Finset.induction_on with

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i
⊢ ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i

Tactic:
exact hs.induction_on hmono hcountable_union h_nhds

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

Goal state before:
pp: case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover ∅ t

Tactic:
exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x y : X
h : ¬Inseparable x y
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst✝¹] V₁ ∧
            IsClosed[inst✝¹] V₂ ∧ IsOpen[inst✝¹] U₁ ∧ IsOpen[inst✝¹] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
by
  rcases r1_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
  rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
  rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
  exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
hne : x ≠ y
this : x ∉ closure[inst✝¹] {y} ∨ y ∉ closure[inst✝¹] {x}
⊢ Disjoint (𝓝 x) (𝓝 y)

Tactic:
simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
hne : x ≠ y
this : Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)
⊢ Disjoint (𝓝 x) (𝓝 y)
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 ?_
      simp only [Set.iUnion_subset_iff]
      intro i hi
      rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
      exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : x ∈ interior s
⊢ False

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
⊢ False
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ

Tactic:
obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x
  use t, tc
  apply top_unique s

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

Goal state before:
pp: case ht'
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ IsConnected (connectedComponent t)

pp: case connected_fibers
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ ∀ (t : β), IsConnected (f ⁻¹' {t})

Tactic:
· exact isConnected_connectedComponent

Goal state after:
case connected_fibers
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ ∀ (t : β), IsConnected (f ⁻¹' {t})
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ∃ i, ¬IsConnected (U i)

Tactic:
simp_rw [isConnected_iff_connectedSpace, ← not_forall]

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
U : Fin (n + 1) → Set α
h₁ : ∀ (i : Fin (n + 1)), IsClopen (U i)
h₂ : ∀ (i : Fin (n + 1)), (U i).Nonempty
h₃ : Pairwise (Disjoint on U)
h₄ : ⋃ i, U i = univ
⊢ ¬∀ (x : Fin (n + 1)), ConnectedSpace ↑(U x)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
g : γ → α
⊢ TendstoUniformly (fun n ↦ F n ∘ g) (f ∘ g) p

Tactic:
tendstoUniformly_iff_tendstoUniformlyOnFilter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p ⊤
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun x ↦ c) p

Tactic:
tendstoUniformly_iff_tendstoUniformlyOnFilter

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p ⊤
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ IsComplete (⋃ i, s i)

Tactic:
by
  set S := ⋃ i, s i
  intro l hl hls
  rw [le_principal_iff] at hls
  obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
  obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left
  obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
    rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
    rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
    refine ⟨i, fun y hy => ?_⟩
    rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
    rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
  rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
  exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ UniformContinuousOn (g ∘ f) s

Tactic:
change Tendsto ((fun x ↦ (g x.1, g x.2)) ∘ (fun x ↦ (f x.1, f x.2))) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)
  apply Tendsto.comp hg
  refine tendsto_inf.2 ⟨hf, tendsto_inf_right ?_⟩
  simp only [tendsto_principal, mem_prod, eventually_principal, and_imp, Prod.forall]
  exact fun a b ha hb ↦ ⟨hst ha, hst hb⟩

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

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
⊢ u = ⊤

Tactic:
refine UniformSpace.ext ?_
  rw [top_uniformity, ← Filter.ker_eq_univ]
  ext x
  rw [← inseparable_iff_ker_uniformity]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
F : Filter α
⊢ Cauchy (map f F) ↔ Cauchy F

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
f : α → β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ CompleteSpace (α ⊕ β)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
f : α → β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ IsComplete (range Sum.inl ∪ range Sum.inr)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ (∃ x_1 ∈ 𝓝 x, Disjoint x_1 (mulSupport f)) ↔ f =ᶠ[𝓝 x] 1

Tactic:
disjoint_mulSupport_iff,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ (∃ x_1 ∈ 𝓝 x, EqOn f 1 x_1) ↔ f =ᶠ[𝓝 x] 1
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst✝², inst✝] f
hk : IsClosed[inst✝] K
h'k : 1 ∉ K
x : α
hx : x ∈ f ⁻¹' K
⊢ x ∈ mulSupport f

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
  obtain
    ⟨t : ℕ → SetRel α α, hto : ∀ i : ℕ, t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ (t i).IsSymm,
      h_basis : (𝓤 α).HasAntitoneBasis t⟩ :=
    (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
  choose ht_mem hto hts using hto
  refine ⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩
  refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom
  · simp only [mem_iUnion₂, mem_range]
    rintro _ ⟨x, _, k, rfl⟩
    exact isOpen_ball x (hto k)
  · intro x V hxV hVo
    simp only [mem_iUnion₂, mem_range, exists_prop]
    rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩
    rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩
    rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩
    rcases hsd.inter_open_nonempty (ball x <| t k) (isOpen_ball x (hto k))
        ⟨x, UniformSpace.mem_ball_self _ (ht_mem k)⟩ with
      ⟨y, hxy, hys⟩
    refine ⟨_, ⟨y, hys, k, rfl⟩, (t k).symm hxy, fun z hz => ?_⟩
    exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))

Goal state after: