mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f f' : Filter α
⊢ ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'

Tactic:
by simp only [iSup_le_iff, ← le_iff_ultrafilter]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
⊢ ∃ b, b.Countable ∧ t = generateFrom b

Tactic:
by
    -- The countable union of the countable neighborhood bases at each point is a countable basis.
    choose b hxb hbb using fun x : α => (nhds_basis_opens x).exists_antitone_subbasis
    use range b.uncurry, countable_range b.uncurry
    apply le_antisymm
    · rw [le_generateFrom_iff_subset_isOpen]
      rintro _ ⟨⟨x, n⟩, rfl⟩
      exact (hxb x n).right
    · rw [le_iff_nhds]
      intro x
      rw [(hbb x).ge_iff]
      intro n _
      refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left
      exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a ↦ f ⟨i, a⟩

Tactic:
simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp_def]

Goal state after:
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 : X
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]

Goal state after:
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ i, p i ∧ q (s i)

Tactic:
l.eventually_smallSets' hq,

Goal state after:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∃ s ∈ l, q s) ↔ ∃ i, p i ∧ q (s i)
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case pos
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)
i : ι
h : i ∈ s
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
rw [if_pos h]
        exact hc i

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_antisymm
    · apply le_generateFrom_iff_subset_isOpen.2
      simp only [iUnion_subset_iff]
      intro u hu v hv
      rw [ht]
      apply isOpen_generateFrom_of_mem
      exact ft u hu hv
    · rw [hs'.eq_generateFrom]
      apply le_generateFrom_iff_subset_isOpen.2
      intro u hu
      rw [← hf u hu, sInter_eq_biInter]
      change IsOpen[generateFrom _] (⋂ i ∈ f u, i)
      apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _
      · apply f_fin u hu
      · intro i hi
        apply isOpen_generateFrom_of_mem
        simp
        grind

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
have : Countable ↑s := countable_coe_iff.mpr hc
  rw [biUnion_eq_iUnion]
  exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)

Tactic:
by
  apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro - ⟨U, U_in_V, rfl⟩
    apply h U (hV.isOpen U_in_V)
  · intro y U y_in_U U_open
    obtain ⟨x, rfl⟩ := h'.surjective y
    let W := π ⁻¹' U
    have x_in_W : x ∈ W := y_in_U
    have W_open : IsOpen W := U_open.preimage h'.continuous
    obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
    have XZ_in_U : π '' Z ⊆ U := (Set.image_mono Z_in_W).trans (image_preimage_subset π U)
    exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, XZ_in_U⟩

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

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

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u_2
A : Set α
D : Set ↑A
⊢ Subtype.val '' (univ \ 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
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
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x

Tactic:
obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
    ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)

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 : map Prod.fst ↑f ≤ 𝓝 x
y : Y
ty : y ∈ t
hy : map Prod.snd ↑f ≤ 𝓝 y
⊢ ∃ x ∈ s ×ˢ t, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s

Tactic:
exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (s.sigma t)

Tactic:
rw [Set.sigma_eq_biUnion]
  exact hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsDiscrete S ↔ ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
isDiscrete_iff_forall_subset_exists_isOpen

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) ↔ ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
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
r : X → X → Prop
inst✝ : CompactSpace X
⊢ IsCompact univ

Tactic:
rw [← range_quot_mk]

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
r : X → X → Prop
inst✝ : CompactSpace X
⊢ IsCompact (range (mk r))
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 X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝[f '' s] f x ≤ map f (pure x)

Tactic:
← hs.nhdsWithin x hx,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝[f '' s] f x ≤ map f (𝓝[s] x)
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 X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst✝¹] s
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ≤ map f (pure x)

Tactic:
← hs.nhdsWithin x hx,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hs' : IsOpen[inst✝¹] s
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ≤ map f (𝓝[s] x)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (IsClosed[inst✝] S ∧ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
isClosed_iff_clusterPt,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ ((∀ (a : X), ClusterPt a (𝓟 S) → a ∈ S) ∧ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
rw [h.symm.nhdsWithin_compl_singleton] at hb
    exact hb.filter_mono nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ

Tactic:
use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty

Tactic:
rw [Set.inter_compl_nonempty_iff]

Goal state after:
case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ interior s = ∅

Tactic:
refine eq_empty_of_forall_notMem fun x hx ↦ ?_

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
⊢ False
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
⊢ s.Infinite

Tactic:
by
  refine fun hsf => hx.1 ?_
  rw [← isOpen_singleton_iff_punctured_nhds]
  exact isOpen_singleton_of_finite_mem_nhds x hs hsf

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
this : Sᶜ ∈ codiscrete X
⊢ False

Tactic:
rw [mem_codiscrete_accPt, compl_compl] at this

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
S : Set X
x : X
h : AccPt x (𝓟 S)
hs : S.Finite
this : ∀ (x : X), ¬AccPt x (𝓟 S)
⊢ False
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a : α
⊢ 𝓝[≠] a ≤ cofinite

Tactic:
by
  refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_
  rcases eq_or_ne a x with rfl | hx
  exacts [self_mem_nhdsWithin, eventually_ne_nhdsWithin hx]

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

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ

case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅
Module: Mathlib.Data.Set.BoolIndicator

Goal state before:
pp: α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅

case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅

case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅

case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[≠] a

Tactic:
rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a ∩ (s ∩ b) = ∅

Tactic:
inter_comm s b,

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a ∩ (b ∩ s) = ∅
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

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

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]
  have := hS.toEncodable
  exact EventuallyLE.countable_iInter fun i => h i i.2

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
x : α
⊢ ∀ (i : Set α), IsOpen[inst✝¹] i ∧ x ∈ i ∧ IsConnected i ↔ i ∈ {s | IsOpen[inst✝¹] s ∧ IsPreconnected s} ∧ x ∈ i

Tactic:
by grind [IsConnected, Set.Nonempty]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : TopologicalSpace.IsTopologicalBasis {s | IsOpen[inst✝] s ∧ IsPreconnected s}
x✝ : α
⊢ ∀ (i : Set α), i ∈ {s | IsOpen[inst✝] s ∧ IsPreconnected s} ∧ x✝ ∈ i ↔ IsOpen[inst✝] i ∧ x✝ ∈ i ∧ IsConnected i

Tactic:
by grind [IsConnected, Set.Nonempty]

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ i ∈ S, ∀ᶠ (x : α) in l, ∀ᶠ (x_1 : β) in m, (x, x_1) ∈ i

Tactic:
← mem_curry_iff

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β✝ : Type u_3
l✝ : Filter α✝
inst✝² : CountableInterFilter l✝
α : Type u_4
β : Type u_5
l : Filter α
m : Filter β
inst✝¹ : CountableInterFilter l
inst✝ : CountableInterFilter m
S : Set (Set (α × β))
Sct : S.Countable
hS : ∀ s ∈ S, s ∈ l.curry m
⊢ ∀ i ∈ S, i ∈ l.curry m
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1.inr.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : (inr '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1

Tactic:
· exact Or.inr ⟨t, ht.isPreconnected, rfl⟩

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

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (s i)ᶜ

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (univ \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (s i)ᶜ

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (univ \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ P x y

Tactic:
apply hs.induction₂' P (fun z hz ↦ ?_) h' hx hy

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
⊢ ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z
Module: Mathlib.Topology.Separation.Regular

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

Tactic:
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

Goal state after:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed[↑↑i] (If.snd i)) fun If ↦
      ⋂ i, If.snd i
⊢ RegularSpace X
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
l : Filter X
inst✝ : CountableInterFilter l
hs : IsLindelof s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
by
  refine ⟨fun h x hx ↦ h.mono_left <| nhds_le_nhdsSet hx, fun H ↦ ?_⟩
  choose! U hxU hUl using fun x hx ↦ (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
  choose hxU hUo using hxU
  rcases hs.elim_nhds_subcover U fun x hx ↦ (hUo x hx).mem_nhds (hxU x hx) with ⟨t, htc, hts, hst⟩
  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx ↦ hUo x (hts x hx), hst⟩, ?_⟩
  rw [compl_iUnion₂]
  exact (countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))

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

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

Tactic:
subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F

Tactic:
split_ifs

Goal state after:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∈ F
⊢ (Subtype.val '' connectedComponent ⟨x, h✝⟩).Nonempty ↔ x ∈ F

case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
h✝ : x ∉ F
⊢ ∅.Nonempty ↔ x ∈ F
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅) ⊆ F

Tactic:
split_ifs

Goal state after:
case pos
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∈ F
⊢ Subtype.val '' connectedComponent ⟨x, h✝⟩ ⊆ F

case neg
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∉ F
⊢ ∅ ⊆ F