mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
s : Set α
t : Set ↑s
x✝ : α
⊢ x✝ ∈ ⋃ x ∈ t, {↑x} ↔ x✝ ∈ Subtype.val '' t

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' Subtype.val '' γ ↔ x✝ ∈ β.domRestrict f '' γ

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset ↑t
⊢ Subtype.val '' ↑a ⊆ t

Tactic:
simp

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

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ Subtype.val '' ↑d ⊆ b

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ ∅ ×ˢ l

Tactic:
simp

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

Goal state before:
pp: case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx)
      with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩

Goal state after:
case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst✝] (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B : Set α
h : A ⊆ B
⊢ A ↓∩ B = univ

Tactic:
eq_univ_iff_forall,

Goal state after:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (x : ↑A), x ∈ A ↓∩ B
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (f a))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ioi a)) ↔ x✝ ∈ ↑(Ioi (f a))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, Ici (f i j)

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ {x} ∈ {s | IsCompact s} ∧ x ∈ {x}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(upperClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Ici a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨅ a ∈ s, Ici a) ↔ x✝ ∈ ↑(upperClosure s)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s ⊆ ↑⊤ ↔ s = ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(upperClosure {a}) ↔ x✝ ∈ ↑(UpperSet.Ici a)

Tactic:
simp

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set ↑P
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, ↑⟨↑i, ⋯⟩
⊢ (fun x ↦ ↑x) '' J ⊆ P

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (UpperSet α)) x✝¹)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ f ≤ 𝓟 univ

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
⊢ ↑F ≤ 𝓟 univ

Tactic:
simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst✝ : f.NeBot
⊢ f ≤ 𝓟 t → ∃ x ∈ t, ClusterPt x f

Tactic:
hf

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst✝ : f.NeBot
hf : f ≤ 𝓟 t
⊢ ∃ x ∈ t, ClusterPt x f
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x ↦ closure[inst✝] {x}) '' s) = ⋃ x ∈ s, closure[inst✝] {x}

Tactic:
simp

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
x : (i : ι) × X i
hx : x ∈ u
⊢ x ∈ ⋃ i, Sigma.mk i '' Sigma.mk i ⁻¹' univ

Tactic:
simp

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

Goal state before:
pp: case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ ∈ cocompact (X × Y)

Tactic:
rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]

Goal state after:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ (K.1 ×ˢ K.2)ᶜ ∈ cocompact (X × Y)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: 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

Tactic:
constructor <;> intro h s sS

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
⊢ ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
⊢ ∃ u, IsOpen[inst✝] u ∧ u ∩ S = s
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 '' s] f x ≤ pure (f x)

Tactic:
rw [(hf _ hs').nhdsWithin_eq ⟨x, hx, rfl⟩, ← map_pure, ← hs.nhdsWithin x hx, hs'.nhdsWithin_eq 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 (𝓝 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
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X

Tactic:
cocompact_eq_cofinite X

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cofinite
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
x : CofiniteTopology X
⊢ {x} = univ ∨ {x}.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ s ∩ U = (sᶜ ∪ Uᶜ)ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
⊢ (S ∩ (a ∩ b)).Nonempty

Tactic:
by_contra! h0

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ False
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
simp

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 : Y → X
h : IsOpenMap f
s : Set X
hne : (f ⁻¹' s).Nonempty
hs : IsPreirreducible s
hs' : IsClosed[inst✝¹] s
⊢ f '' f ⁻¹' s ⊆ s

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ (Sum.inl x).isLeft ≠ (Sum.inr y).isLeft

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ (Sum.inr x).isLeft ≠ (Sum.inl y).isLeft

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
x : X
⊢ (⇑CofiniteTopology.of '' {x}).Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ (insert z ∅).Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ ∅.Finite

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s

Tactic:
nhdsSet_le_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ {x} ⊆ s ↔ x ∈ s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝 z
h₂t : (t ∩ (U \ s)).Finite
⊢ t \ (t ∩ (U \ s)) ∩ (U \ s) = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case empty
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∅ᶜ ∈ codiscreteWithin s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b ⊆ {a}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b ⊆ {b}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : NoBotOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: 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 ∩ (s ∩ a)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Continuous[inst✝², inst✝¹] fun x ↦ if f x ≤ g x then f' x else g' x

Tactic:
refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ ContinuousOn f' (closure[inst✝²] {x | f x ≤ g x})

case refine_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ closure[inst✝²] {x | ¬f x ≤ g x} ⊆ {x | g x ≤ f x}
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsClopen t
hne : (s ∩ t).Nonempty
⊢ s ⊆ t ∪ tᶜ

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
z : X i
x✝ : z ∈ univ
⊢ Function.eval i (Function.update x i z) = z

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s : Set α
⊢ ∅ ⊆ g ∧ ∅.Countable ∧ ⋂₀ ∅ ⊆ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
by
  refine ⟨fun hs => ?_, ?_⟩
  · obtain rfl | h := s.eq_empty_or_nonempty
    · exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩
    obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩
    · exact Or.inl ⟨t, ht.isPreconnected, rfl⟩
    · exact Or.inr ⟨t, ht.isPreconnected, rfl⟩
  · rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)
    · exact ht.image _ continuous_inl.continuousOn
    · exact ht.image _ continuous_inr.continuousOn

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

Goal state before:
pp: α : Type u_2
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}

Tactic:
rintro f ⟨fct, hf⟩

Goal state after:
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : 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 \ s i)

Tactic:
simp

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

Goal state before:
pp: case inl
α : 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 \ s i)

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
hcountable_union :
  ∀ (S : Set (Set X)),
    S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i
x : X
hx : x ∈ s
i : ι
hi : x ∈ U i
⊢ {i}.Countable

Tactic:
simp

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

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.rwSeq
   "rw"
   (Tactic.optConfig [])
   (Tactic.rwRuleSeq "[" [(Tactic.rwRule ["←"] `not_nonempty_iff_eq_empty)] "]")
   [(Tactic.location "at" (Tactic.locationHyp [`hsuv]))])
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hsuv)))
  ";"
  (Tactic.rwSeq
   "rw"
   (Tactic.optConfig [])
   (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.app `inter_comm [`u]))] "]")
   [(Tactic.location "at" (Tactic.locationHyp [`this]))])
  []
  (Tactic.simpa
   "simpa"
   []
   []
   (Tactic.simpaArgsRest
    (Tactic.optConfig [])
    []
    []
    [(Tactic.simpArgs
      "["
      [(Tactic.simpStar "*") "," (Tactic.simpLemma [] [] `or_imp) "," (Tactic.simpLemma [] [] `forall_and)]
      "]")]
    ["using"
     (Term.app
      `h
      [(choice
        («term{_}» "{" [`u "," `v] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields
          [(Term.structInstField (Term.structInstLVal `u []) [])
           ","
           (Term.structInstField (Term.structInstLVal `v []) [])])
         (Term.optEllipsis [])
         []
         "}"))])]))])

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

Goal state before:
pp: case univ
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
ha : a ∈ univ
⊢ Disjoint (𝓝ˢ univᶜ) (𝓝 a)

Tactic:
simp

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Set ↑b
hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i
⊢ Subtype.val '' d ⊆ b

Tactic:
simp

Goal state after: