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

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ (∃ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ {x}ᶜ ∧ x_1 ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ

Tactic:
by simp only [and_comm]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case inl
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := ⋯
x₃' : α := ⋯
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ + p ∈ Set.Ioc x₂' (x₂' + p) ∧ ∃ z, x₁ = x₁ + p + z • p

Tactic:
exact ⟨⟨h₂₁, by simp [x₂', left_le_toIcoMod]⟩, -1, by simp⟩

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst✝]

Tactic:
by
  simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)

Tactic:
rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
    sub_right_comm _ _ a]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p x ∈ U

Tactic:
← hg ((congr_fun h y).trans e')

Goal state after:
case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p y ∈ U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
g : Set (Set α)
a : α
⊢ 𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Tactic:
let := generateFrom g
  rw [nhds_def]
  refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_
  rintro s ⟨ha, hs⟩
  induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ pure x ↔ x ∈ s

Tactic:
mem_pure

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ x ∈ s ↔ x ∈ s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤

Tactic:
by
  simp_rw [nontrivialTopology_iff, topology_eq_induced, ne_eq, not_iff_not]
  constructor
  · intro h
    simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)
  · simp +contextual

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, _] f

Tactic:
simp only [continuous_iff_coinduced_le, le_sInf_iff]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap '' s)

Tactic:
rw [image_swap_eq_preimage_swap]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap ⁻¹' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
z : α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓝 z, x ∈ s ∧ p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s

Tactic:
by simp only [and_comm]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
by
  rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ 𝓝 (x, y) = map Prod.swap (𝓝 (y, x))

Tactic:
rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
⊢ (∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)) →
    ∀ (s : Set Y), IsOpen[inst✝] s → IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
intro hf t ht

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : ∀ (a : X), f a ∈ s
hf : ∀ (s_1 : Set ↑s), IsOpen[instTopologicalSpaceSubtype] s_1 → IsOpen[inst✝¹] (codRestrict f s hs ⁻¹' s_1)
t : Set Y
ht : IsOpen[inst✝] t
⊢ IsOpen[inst✝¹] (f ⁻¹' t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis {∅}
⊢ IsEmpty α

Tactic:
simpa using h.sdiff_empty

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
⊢ ⇑(partialSups f) = accumulate f

Tactic:
ext n

Goal state after:
α : Type u_1
f : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups f) n ↔ x✝ ∈ accumulate f n
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n : ℕ
⊢ ∃ m, accumulate s n ⊆ s m

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
⊢ IsBounded ∅

Tactic:
rw [isBounded_def, compl_empty]

Goal state after:
α : Type u_2
x✝ : Bornology α
⊢ univ ∈ cobounded α
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ ∅ ∈ cobounded α

Tactic:
empty_mem_iff_bot

Goal state after:
α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ cobounded α = ⊥
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case refine_3
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ IsCompact (s.pi n'')

Tactic:
rw [← Set.univ_pi_ite]
      refine isCompact_univ_pi fun i => ?_
      by_cases h : i ∈ s
      · rw [if_pos h]
        exact hc i
      · rw [if_neg h]
        exact CompactSpace.isCompact_univ

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (n, y).1 (n, y).2 = f (N (n, y).2 + 1) (n, y).2

Tactic:
calc
    f n y = f (N x + 1) y := hN _ _ hn _ hy
    _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
    _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)

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

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

Tactic:
contrapose! hst
  exact hs.elim_finite_subfamily_closed t htc hst

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
simp [nhds_discrete]

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact univ

Tactic:
rw [← univ_prod_univ]

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst✝] s
hs' : IsOpen[inst✝] s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'

Tactic:
simpa [hx] using Set.ext_iff.1 ht x

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:
← ite_compl,

Goal state after:
α : 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ᶜ
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
⊢ (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty

Tactic:
⟨p, pS, pa⟩

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
⊢ (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, sᶜ ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
simp_all [← Set.compl_sdiff, mem_codiscreteWithin]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst✝²] s
⊢ EqOn f g t

Tactic:
by
  intro x hx
  have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
  exact
    tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
t : Set X
h₁t : ∀ y ∈ t, f y ≠ g y
h₂t : IsOpen[inst✝²] t
h₃t : x ∈ t
⊢ f x ≠ g x

Tactic:
exact h₁t x h₃t

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
by
  rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩

Tactic:
simp [nhds_discrete]

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

Goal state before:
pp: case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨x, htop x hx, le_rfl⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)

Tactic:
refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
simp [nhds_discrete]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : PreconnectedSpace α
inst✝ : PreconnectedSpace β
⊢ IsPreconnected univ

Tactic:
rw [← univ_prod_univ]

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : PreconnectedSpace α
inst✝ : PreconnectedSpace β
⊢ IsPreconnected (univ ×ˢ univ)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsLindelof K
⊢ IsLindelof (f ⁻¹' K)

Tactic:
by
  replace hK := hK.inter_right hf'
  rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ φ x ∈ V'

Tactic:
apply V'_closed.mem_of_tendsto x_in₁

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := ⋯
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := ⋯
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i

Tactic:
have : IsLindelof (⋃ i, U i) := HereditarilyLindelofSpace.isLindelof (⋃ i, U i)

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝¹] (U i)
this : IsLindelof (⋃ i, U i)
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
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 : β
⊢ IsConnected (f ⁻¹' connectedComponent t)

Tactic:
by
  apply hcl.isConnected_preimage_of_isClosed
  · exact isClosed_connectedComponent
  · exact isConnected_connectedComponent
  · exact connected_fibers

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)

Tactic:
by
  rcases S.eq_empty_or_nonempty with h | h
  · simp [h]
  · rcases hS.exists_eq_range h with ⟨f, rfl⟩
    exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

Goal state after:
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
U : SetRel X X
N : Set X
⊢ U.IsCover ∅ N

Tactic:
simp [IsCover]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ ∀ (s : Set X), IsClosed[inst✝³] s → IsClosed[inst✝²] (⇑f.symm ⁻¹' s)

Tactic:
intro C

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
C : Set X
⊢ IsClosed[inst✝³] C → IsClosed[inst✝²] (⇑f.symm ⁻¹' C)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
⊢ ∃ U,
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

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

Goal state before:
pp: β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β

Tactic:
rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

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

Goal state before:
pp: β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}

Tactic:
mem_ball_symmetry

Goal state after:
β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W

Tactic:
mem_ball_symmetry

Goal state after:
β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y z : β
hzy : (z, y) ∈ W
w : β
hpw : (x, w) ∈ V
hwz : (w, z) ∈ M
⊢ (w, z).2 ∈ ball (x, y).2 W

Tactic:
mem_ball_symmetry

Goal state after:
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y z : β
hzy : (z, y) ∈ W
w : β
hpw : (x, w) ∈ V
hwz : (w, z) ∈ M
⊢ (x, y).2 ∈ ball (w, z).2 W
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (w, z).2 ∈ ball (x, y).2 W
⊢ (x, y) ∈ V ○ M ○ W

Tactic:
mem_ball_symmetry

Goal state after:
case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
inst✝ : UniformSpace β
T : β → β
n : ℕ
h : UniformContinuous T
⊢ UniformContinuous T^[n]

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝 x

Tactic:
apply mem_of_superset (ball_mem_nhds x (hB.mem (U b ⟨x, hx⟩)))

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := ⋯
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
b : Bool
x : α
hx : x ∈ S b
⊢ ball x (B (U b ⟨x, hx⟩)) ⊆ ⋃ x, ball (↑x) (B (U b x))
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
by simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
    iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ comap (fun x ↦ (inclusion hst x.1, inclusion hst x.2)) (𝓤 ↑t) = 𝓤 ↑s

Tactic:
by rw [uniformity_subtype, uniformity_subtype, comap_comap]; rfl

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Tactic:
rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_filter]

Goal state after:
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
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : x ∈ ball a V
b : α
hb : b ∈ B
hxb : x ∈ ball b V
⊢ False

Tactic:
mem_ball_symmetry

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 : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : a ∈ ball x V
b : α
hb : b ∈ B
hxb : b ∈ ball x V
⊢ False