mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
⊢ IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f ↦ f)

Tactic:
rw [isSeparator_def]
  refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
  · simpa using Sigma.ι _ i ≫= huv
  · have := h X
    refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)
    simpa using hh j.as

Goal state after:
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = n ↔ ∀ n' < n, p n'

Tactic:
by
  simpa [count_eq_card_filter_range, card_range, mem_range] using
    card_filter_eq_iff (p := p) (s := range n)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr.hbd
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

pp: case inr.hc
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 0 < (c ^ 2)!

Tactic:
· exact Nat.pow_lt_pow_left (Nat.lt_succ_self _) (Nat.succ_ne_zero _)

Goal state after:
case inr.hc
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 0 < (c ^ 2)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
let d := a.gcd b
  rcases eq_zero_or_pos a with (rfl | ha0)
  · simp
  have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
  apply le_of_mul_le_mul_right _ hd0
  grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p q : X → Prop
hp : IsOpen[inst✝] {x | p x}
hq : IsClosed[inst✝] {x | q x}
⊢ IsClosed[inst✝] {x | p x → q x}

Tactic:
by
  simpa only [imp_iff_not_or] using! hp.isClosed_compl.union hq

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ c - b = (toIocDiv hp a c - toIocDiv hp a b) • p

Tactic:
conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]

Goal state after:
case refine_1
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p) =
    (toIocDiv hp a c - toIocDiv hp a b) • p
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
P : Set X → Prop
hP : ∀ (s t : Set X), s ⊆ t → P s → P t
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝] i → P i) ↔ ∀ (s : Set X), IsOpen[inst✝] s → x ∈ s → P s

Tactic:
by simp only [@and_comm (x ∈ _), and_imp]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst✝¹] s ⊆ closure[inst✝] (f '' s)
s : Set Y
hs : IsClosed[inst✝] s
⊢ f ⁻¹' closure[inst✝] (f '' f ⁻¹' s) ⊆ f ⁻¹' s

Tactic:
image_preimage_subset,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst✝¹] s ⊆ closure[inst✝] (f '' s)
s : Set Y
hs : IsClosed[inst✝] s
⊢ f ⁻¹' closure[inst✝] s ⊆ f ⁻¹' s
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 : α
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Tactic:
rw [toIcoMod_eq_iff, and_iff_left]
  exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
Set.inter_union_compl s t

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s = 𝓝ˢ s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Icc (n • p) ((n + 1) • p) = univ

Tactic:
by
  simpa only [zero_add] using iUnion_Icc_add_zsmul hp 0

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_4
β : Type u_5
e : α ≃ β
⊢ TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e

Tactic:
ext t U

Goal state after:
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen[TopologicalSpace.induced (⇑e.symm) t] U ↔ IsOpen[TopologicalSpace.coinduced (⇑e) t] U
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
hf : Continuous[inst✝², inst✝¹] f
f_surj : Surjective f
h : IsOpenMap (g ∘ f)
s : Set Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (g '' s)

Tactic:
rw [← f_surj.image_preimage s, ← image_comp]
  exact h _ (hs.preimage hf)

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (f ⁻¹' ⋃ x ∈ s, {x})

Tactic:
preimage_iUnion,

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
H : ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})
s : Set Y
⊢ comap f (𝓝ˢ (⋃ x ∈ s, {x})) ≤ 𝓝ˢ (⋃ i ∈ s, f ⁻¹' {i})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ IsClosed s ↔ s = univ ∨ s.Finite

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u

Tactic:
intro a u ha uo

Goal state after:
case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
⊢ ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u
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
⊢ closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ

Tactic:
closure_union,

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
⊢ closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (↑f ⊓ g).NeBot

Tactic:
by rwa [inf_comm]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
preimage_image_sigmaMk_of_ne hne

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsOpen[inst✝ j] ∅
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] (Sigma.mk j ⁻¹' Sigma.mk i '' s)

Tactic:
preimage_image_sigmaMk_of_ne hne

Goal state after:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsClosed[inst✝ i] s
j : ι
hne : j ≠ i
⊢ IsClosed[inst✝ j] ∅
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ 𝓝 ⟨i, x⟩ = comap f (𝓝 (f ⟨i, x⟩))

Tactic:
Sigma.nhds_mk,

Goal state after:
case refine_2
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
x✝¹ : (∀ (i : ι), IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
h₁ : ∀ (i : ι), IsInducing (f ∘ Sigma.mk i)
h₂ : ∀ (i : ι), ∃ U, IsOpen[inst✝] U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
x✝ : Sigma σ
i : ι
x : σ i
⊢ map (Sigma.mk i) (𝓝 x) = comap f (𝓝 (f ⟨i, x⟩))
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
by
    refine hf.surjective.forall.2 fun x ↦ ?_
    rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩
    exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Tactic:
refine ⟨t, htx, htf.preimage <| ?_⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ InjOn g (g ⁻¹' {i | (f i ∩ t).Nonempty})
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ n, L n) ∩ s

Tactic:
preimage_iUnion,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, f ⁻¹' L n ∩ s = (⋃ i, f ⁻¹' L i) ∩ s
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ¬K.shiftr.find x ≤ K.find x

Tactic:
by simp only [find_shiftr, not_le, Nat.lt_succ_self]

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rcases hl with ⟨i, his, hi⟩

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst✝] sᶜ)

Tactic:
refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst✝] sᶜ)

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure[inst✝] sᶜ)
⊢ ∃ i, (IsClosed[inst✝] i ∧ IsCompact i) ∧ iᶜ ⊆ s
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
by
  rw [hs.nhdsSetWithin_prod_eq ht, nhdsSetWithin_self, Filter.mem_prod_iff] at hn
  obtain ⟨s', hs', u, hu, h⟩ := hn
  exact ⟨u, hu, (prod_mono_left hs').trans h⟩

Goal state after:
Module: Mathlib.Topology.Irreducible

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

Tactic:
inter_comm s v',

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
w✝ : Set X
rp : IsClosed[inst✝] w✝
rt : w✝ ∩ t = s
⊢ IsClosed[inst✝] s

Tactic:
rw [← rt]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
sd : s ⊆ t
ht : IsDiscrete t
tc : IsClosed[inst✝] t
w✝ : Set X
rp : IsClosed[inst✝] w✝
rt : w✝ ∩ t = s
⊢ IsClosed[inst✝] (w✝ ∩ t)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: 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}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
x✝ : X
⊢ x✝ ∈ (⋃₀ c)ᶜ ↔ x✝ ∈ ⋂ U, (↑U)ᶜ

Tactic:
simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]

Goal state after:
Module: Mathlib.Topology.Irreducible

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
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty

Tactic:
exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
a✝² : X
a✝¹ : ∀ᶠ (x : X) in 𝓝[s] a✝², p x
a✝ : a✝² ∈ s
⊢ ∀ᶠ (x : X) in 𝓝 a✝², p x

Tactic:
simp_all [IsOpen.nhdsWithin_eq]

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
    intro h x U hxU
    rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
    exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩

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
⊢ IsPreconnected (f '' s)

Tactic:
rintro u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩

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
huv : f '' s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hsu

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
⊢ (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hsu

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
⊢ (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
⊢ RegularSpace X

Tactic:
by
  let _ := sInf T
  have : ∀ a, (𝓝 a).HasBasis
      (fun If : Σ I : Set T, I → Set X =>
        If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
      fun If => ⋂ i : If.1, If.snd i := fun a ↦ by
    rw [nhds_sInf, ← iInf_subtype'']
    exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
  refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_
  exact (hIf.2 i).2.mono (sInf_le (i : T).2)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (connectedComponentIn F x).Nonempty ↔ x ∈ F

Tactic:
rw [connectedComponentIn]
  split_ifs <;> simp [connectedComponent_nonempty, *]

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

Goal state before:
pp: case h.left
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
r : ι → Set i
hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2
⊢ (⋃ i_1 ∈ s, r i_1).Countable

Tactic:
refine (Countable.biUnion_iff hs).mpr ?h.left.a
    exact fun s hs ↦ (hr s hs).1

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s

Tactic:
by
  refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩
  rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
  trivial

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

Goal state before:
pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
· exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hT hc hTm hx' hx⟩

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

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : ι → Type u_8
Y : κ → Type u_9
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : κ) → TopologicalSpace (Y i)
f : ι → κ
hf : Bijective f
g : (i : ι) → X i → Y (f i)
hg : ∀ (i : ι), IsHomeomorph (g i)
⊢ IsHomeomorph (Sigma.map f g)

Tactic:
simp_rw [isHomeomorph_iff_isEmbedding_surjective] at hg ⊢
  exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

pp: case hh
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}

Tactic:
· exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩

Goal state after:
case hh
α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s ↦ {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOn F p s
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
u : ℕ → ι × α
h : Tendsto (fun q ↦ (f q.2, F (u q.1).1 q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)
hu : Tendsto (fun n ↦ (u n).1) atTop l ∧ Tendsto (fun n ↦ (u n).2) atTop (𝓟 s)
⊢ Tendsto ((fun q ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)

Tactic:
exact h.comp (tendsto_id.prodMk hu.2)

Goal state after: