mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p

Tactic:
← toIcoMod_le_toIocMod,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] → (pure x ⊓ F.lift' closure[inst✝]).NeBot

Tactic:
intro h
    simp [h, pure_neBot]

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 = a + ((b - a) / p - ↑⌊(b - a) / p⌋) * p

Tactic:
simp [field, -Int.self_sub_floor]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ↑⌊(b - a) / p⌋ * p = a + (b - a - ↑⌊(b - a) / p⌋ * p)
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 - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p

Tactic:
simp [field, -Int.self_sub_floor]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)

Tactic:
hgx

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 x) = map f (𝓝 x)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt,
    and_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] ↑x ⊓ 𝓟 S).NeBot

Tactic:
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩

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

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

Tactic:
compl_univ,

Goal state after:
α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ ∅ ∈ cobounded α
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)

Tactic:
exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.refine_1
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, U i ∈ T i

pp: case refine_2.refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, a ∈ U i

pp: case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u

Tactic:
· exact fun i hi ↦ (hU i hi).1

Goal state after:
case refine_2.refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, a ∈ U i

case refine_2.refine_3
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)

Tactic:
rw [eq, induced_generateFrom_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
by
  rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
    ⟨s, hsc, hsU⟩
  suffices ⋃ x ∈ s, interior (f x) = univ from
    ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
  simp only [hsU, eq_univ_iff_forall, mem_iUnion]
  exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

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

Goal state before:

Tactic:
⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n) ∩ s := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ SigmaCompactSpace ((i : ι) → X i)

Tactic:
refine ⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n,
    fun n => isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩
  rw [iUnion_univ_pi_of_monotone]
  · simp only [iUnion_compactCovering, pi_univ]
  · exact fun i => compactCovering_subset (X i)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝ˢ {y})

Tactic:
exact hs.tendsto_nhdsSet_of_mapClusterPt hmem h

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this✝ : (⋂ i, V i ∩ Wᶜ).Nonempty
this : ¬⋂ i, V i ⊆ W
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b

Tactic:
rwa [← hs.eq has h (hab.trans hbx)]

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
by
  refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_
  obtain hat | hat := em (a ∈ t)
  · exact subset_union_right (subset_upperClosure hat)
  · refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hab⟩
    exact hat <| hst _ ha _ hb hab

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ f x ⤳ f y ↔ x ⤳ y

Tactic:
simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
    mem_preimage]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (f '' closure[inst✝¹] {x})

Tactic:
rw [(specializingMap_iff_closure_singleton hf).mp h x]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
h : SpecializingMap f
x : X
⊢ IsClosed[inst✝] (closure[inst✝] {f x})
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:
by rw [← univ_prod_univ]; exact isCompact_univ.prod isCompact_univ

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
⊢ ∃ s t, s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma t = u

Tactic:
use s, fun i ↦ Sigma.mk i ⁻¹' u, s.finite_toSet, fun i ↦ ?_, ?_

Goal state after:
case left
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
i : ι
⊢ IsCompact (Sigma.mk i ⁻¹' u)

case right
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
⊢ ((↑s).sigma fun i ↦ Sigma.mk i ⁻¹' u) = u
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)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ 𝓝[f ⁻¹' s] x ≤ pure x

Tactic:
← map_le_map_iff hf',

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)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ map f (𝓝[f ⁻¹' s] x) ≤ map f (pure x)
Module: Mathlib.Topology.Irreducible

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

Tactic:
Finset.coe_insert,

Goal state after:
case refine_1.insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
a✝ : u ∉ U
IH : (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
hu : ∀ u_1 ∈ insert u U, IsOpen[inst✝] u_1
hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty
⊢ (s ∩ ⋂₀ insert u ↑U).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed[inst✝] z₁ → IsClosed[inst✝] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_
  simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
  refine forall₂_congr fun _ _ => ?_
  rw [← and_imp, ← not_or, not_imp_not]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Tactic:
simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    Set.mem_sdiff, mem_inter_iff, mem_compl_iff]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ (∀ i ∈ T, ∃ u, IsOpen[inst✝] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ u, IsOpen[inst✝] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝¹ s✝))

Tactic:
Finset.coe_insert,

Goal state after:
case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ insert a✝¹ ↑s✝)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂

Tactic:
have : SeparatedNhds (K \ U) (K \ V) :=
    this.mono (sdiff_subset_sdiff_left (subset_closure)) (sdiff_subset_sdiff_left (subset_closure))

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hV : IsOpen[inst✝¹] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst✝¹] K)
this✝ : SeparatedNhds (closure[inst✝¹] K \ U) (closure[inst✝¹] K \ V)
this : SeparatedNhds (K \ U) (K \ V)
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ i, Iic (f i) = Iio a

Tactic:
by
  have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
  rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ IsPreconnected (⋃₀ c)

Tactic:
apply isPreconnected_of_forall x
  rintro y ⟨s, sc, ys⟩
  exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V

Tactic:
simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
Module: Mathlib.Topology.Connected.Basic

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

Tactic:
rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)

Goal state after:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
y : β
hy : y ∈ t
⊢ (a₁, y) ∈ s ×ˢ t

case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsPreconnected s
ht : IsPreconnected t
a₁ : α
b₁ : β
ha₁ : (a₁, b₁).1 ∈ s
hb₁ : (a₁, b₁).2 ∈ t
a₂ : α
b₂ : β
ha₂ : (a₂, b₂).1 ∈ s
hb₂ : (a₂, b₂).2 ∈ t
x : α
hx : x ∈ s
⊢ flip Prod.mk b₂ x ∈ s ×ˢ t
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ s ⊆ (⋂ i, t i)ᶜ

Tactic:
apply disjoint_compl_left_iff_subset.mp

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := ⋯
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ Disjoint (⋂ i, t i)ᶜᶜ s
Module: Mathlib.Topology.Compactness.Lindelof

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

Tactic:
rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
u : Set ι
left✝ : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅
Module: Mathlib.Topology.Compactness.Lindelof

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

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val ⁻¹' s)

Tactic:
refine IsInducing.subtypeVal.isPreconnected_image.mp ?_

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val '' Subtype.val ⁻¹' s)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen[inst✝] s → NormalSpace ↑s

Tactic:
refine ⟨fun _ _ _ => inferInstance, fun h => ⟨fun s t hSt hsT => ?_⟩⟩
  let e := (closure s ∩ closure t)ᶜ
  have he : IsOpen e := (isClosed_closure.inter isClosed_closure).isOpen_compl
  specialize h e he
  have hst : Disjoint (((↑) : e → X) ⁻¹' closure s) (((↑) : e → X) ⁻¹' closure t) := by
    rw [disjoint_left]
    intro x hxs hxt
    exact x.2 ⟨hxs, hxt⟩
  obtain ⟨U, V, hU, hV, hsU, htV, hUV⟩ := normal_separation
    (isClosed_closure.preimage continuous_subtype_val)
    (isClosed_closure.preimage continuous_subtype_val) hst
  rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV
  obtain ⟨U, hU, rfl⟩ := hU
  obtain ⟨V, hV, rfl⟩ := hV
  rw [← separatedNhds_iff_disjoint]
  rw [Subtype.preimage_val_subset_preimage_val_iff, inter_comm e, inter_comm e] at hsU htV
  refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩
  · intro x hx
    exact hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩
  · intro x hx
    exact htV ⟨subset_closure hx, fun h => hSt.notMem_of_mem_left h.1 hx⟩
  · rw [disjoint_left] at hUV ⊢
    intro x hxU hxV
    exact @hUV ⟨x, hxU.2⟩ hxU.1 hxV.1

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ x, t ↑x ⋯)

Tactic:
have := hs.to_subtype

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Countable ↑s
⊢ IsGδ (⋂ x, t ↑x ⋯)