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

Goal state before:
pp: case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b

pp: case inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b

Tactic:
· exact hs

Goal state after:
case inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
simp only [← isOpen_compl_iff, isOpen_induced_iff]

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen[t] t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s
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:
by rw [hgx]

Goal state after:
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
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst✝] (kernImage f s) ⊆ kernImage f (closure[inst✝¹] s)

Tactic:
rw [isOpenMap_iff_image_interior, compl_surjective.forall]
  simp [kernImage_eq_compl]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[∅] a = ⊥

Tactic:
rw [nhdsWithin, principal_empty, inf_bot_eq]

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:
Filter.prod_comm,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ map Prod.swap (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 (y, x))
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u

Tactic:
← prod_iUnion,

Goal state after:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ u ×ˢ ⋃ i ∈ t, i = Prod.fst ⁻¹' u
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ DenseRange (Pi.map f)

Tactic:
by
  rw [DenseRange, Set.range_piMap]
  exact dense_pi Set.univ (fun i _ => hf i)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
ht : ContinuousWithinAt f t x
h : ContinuousWithinAt f (s \ t) x
⊢ s ⊆ s \ t ∪ t

Tactic:
by simp only [sdiff_union_self, subset_union_left]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id
t₁ : Set α
ht₁ : t₁ ∈ s
t₂ : Set α
ht₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simpa only [and_assoc, (h_nhds x).mem_iff]
      using! (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃ i, ↑i

Tactic:
rw [← sUnion_eq_iUnion]
    apply hB.open_eq_sUnion' ou

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s

Tactic:
inter_eq_self_of_subset_left (image_mono inter_subset_right),

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x = ⋃ x, s x

Tactic:
apply Subset.antisymm
  · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
    intro z x x' ⟨_, hz⟩
    exact ⟨x', hz⟩
  · exact iUnion_mono fun i => subset_accumulate

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B

Tactic:
rw [sUnion_eq_univ_iff] at sUnion_univ
    rcases sUnion_univ x with ⟨s, hs, hxs⟩
    exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
have ⟨w, hw⟩ := continuousOn_iff'.1 hf v hv.1

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ Sum.inr '' univ = univ

Tactic:
image_univ,

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ range Sum.inl ∪ range Sum.inr = univ
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I).pi t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ I.piecewise x y i ∈ t i

Tactic:
simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] ((↑i).pi t ∩ (↑i)ᶜ.pi c)

Tactic:
← univ_pi_piecewise

Goal state after:
case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] (univ.pi ((↑i).piecewise t c))
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

Tactic:
obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : (↑s).pi U = ∅
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)

case inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen[inst✝ i] (eval i '' (↑s).pi U)
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst✝², inst✝¹] f
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : MapsTo f K U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
    exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))
  rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩
  exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦
    hVU x (hsK x hx)⟩

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i ↦ closure[inst✝] (f i)

Tactic:
intro x
  rcases hf x with ⟨s, hsx, hsf⟩
  refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩
  exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
    (inter_subset_inter_right _ interior_subset)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' univ)

Tactic:
image_univ,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact (range Subtype.val)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i

Tactic:
rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x
t : ℕ → Finset X
ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s
hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}
x : X
hx : x ∈ s
n : ℕ
hn : x ∈ compactCovering X n
y : X
hyt : y ∈ t n
hyf : x ∈ s → x ∈ f y
⊢ ∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
by
  simp only [nhdsWithin, mem_inf_principal] at hf
  choose t ht hsub using fun n =>
    ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right
  refine
    ⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
      countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩
  rcases exists_mem_compactCovering x with ⟨n, hn⟩
  rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
  exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩

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

Goal state before:
pp: α : Type u_2
A : Set α
D : Set ↑A
⊢ Subtype.val '' univ \ Subtype.val '' D = A \ Subtype.val '' D

Tactic:
image_univ,

Goal state after:
α : Type u_2
A : Set α
D : Set ↑A
⊢ range Subtype.val \ Subtype.val '' D = A \ Subtype.val '' D
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
⊢ ∀ [l.NeBot], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
hne

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
⊢ l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ Ici a ⊓ s.erase a = s

Tactic:
rw [inf_comm, erase_inf_Ici ha has]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf
  calc
    f ×ˢ 𝓝ˢ t
    _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ principal_le_nhdsSet
    _ = 𝓝ˢ (K ×ˢ t) := (hK.nhdsSet_prod_eq ht).symm
    _ ≤ 𝓝ˢ (Set.univ ×ˢ t) := nhdsSet_mono (prod_mono_left le_top)

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ⋃₀ P = univ
⊢ ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ

Tactic:
contrapose! hP

Goal state after:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → ⋃₀ Q ≠ univ
⊢ ⋃₀ P ≠ univ
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✝ : NoncompactSpace X
⊢ (cocompact X).NeBot

Tactic:
refine Filter.hasBasis_cocompact.neBot_iff.2 fun hs => ?_
  contrapose hs; rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
  rw [hs]; exact noncompact_univ X

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact (Subtype.val '' univ)

Tactic:
image_univ,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact (range Subtype.val)
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 : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst ↑f ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd ↑f ≤ 𝓝 y
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
rw [map_le_iff_le_comap] at hx hy

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
A : ι → Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : (i : ι) → TopologicalSpace (A i)
x y z : X
s : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
p : α → Prop
⊢ IndiscreteTopology (Subtype p)

Tactic:
by
  simp [TopologicalSpace.indiscrete_iff_forall_inseparable, subtype_inseparable_iff]

Goal state after:
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₂ => ?_

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsOpen[inst✝] z₁ᶜ → IsOpen[inst✝] z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed[inst✝] z₁ → IsClosed[inst✝] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
hne : x ≠ y
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, Disjoint (𝓝 x) (𝓝ˢ L)

Tactic:
hL.disjoint_nhdsSet_right,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, Disjoint (𝓝 x) (𝓝 x_1)
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simpa only [Filter.Eventually, ofPred_forall] using
    @countable_iInter_mem _ _ l _ _ fun i => { x | p x i }

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst✝] u
hu' : IsOpen[inst✝¹] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst✝] v
hv' : IsOpen[inst✝¹] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v
⊢ f '' s ⊆ u ∪ v

Tactic:
rwa [image_subset_iff]

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

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
h'x : x ∈ closure[inst✝] u
⊢ False

Tactic:
exact xu (h (mem_inter h'x hx))

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

Goal state before:
pp: case sUnion
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t✝ : Set X
S : Set (Set X)
a✝ : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, a ∈ s → Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
exact ih t ht ha

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

Goal state before:
pp: 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
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
by
  obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU
  rcases c.eq_empty_or_nonempty with rfl | c_nonempty
  · 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]
  obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count
  refine ⟨fun x ↦ f x, c_cov.trans <| iUnion₂_subset_iff.mpr (?_ : ∀ i ∈ c, U i ⊆ ⋃ n, U (f n))⟩
  intro x hx
  obtain ⟨n, hn⟩ := f_surj ⟨x, hx⟩
  exact subset_iUnion_of_subset n <| subset_of_eq (by rw [hn])

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected (val '' univ)

Tactic:
image_univ,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ IsPreconnected (range val)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
⊢ ∀ [l.NeBot] [CountableInterFilter l], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
hne

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
⊢ ∀ [CountableInterFilter l], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ IsLindelof (Subtype.val '' univ)

Tactic:
image_univ,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsLindelof s ↔ IsLindelof (range Subtype.val)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)

Tactic:
induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsOpen[inst✝] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
compl_bijective.surjective.image_surjective.exists

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ x,
      (∀ t ∈ compl '' x, IsOpen[inst✝] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S