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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a

Tactic:
by
  delta nhdsWithin
  rw [← inf_sup_left, sup_principal]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Tactic:
rw [nhdsWithin_prod_eq]
  exact prod_mem_prod hu hv

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
by
  simp_rw [nhdsWithin_eq, tendsto_iInf, mem_ofPred_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h
  exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing fun x ↦ (f x, y)) ↔ IsInducing f

Tactic:
by
  simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_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
⊢ IsClosed[instTopologicalSpaceSum] (range inl)

Tactic:
rw [← isOpen_compl_iff, compl_range_inl]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s✝ s : Set α
⊢ s ∈ 𝓝ˢ s✝ ↔ s ∈ comap f (𝓝ˢ (f '' s✝))

Tactic:
rw [mem_nhdsSet_induced, mem_comap]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : Set ↑s
⊢ map Subtype.val (𝓝ˢ t) = 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
rw [IsInducing.subtypeVal.map_nhdsSet_eq, Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsOpen[t] ∅

pp: case inr
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
u✝ : Set α
hu : u✝ ∈ s
⊢ IsOpen[t] u✝

Tactic:
exacts [isOpen_empty, h.isOpen hu]

Goal state after:
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 : (a : ι) → A a
hs : s ∈ 𝓝 x
y : (a : ι) → A a
⊢ ∃ I, I.piecewise x y ∈ s

Tactic:
simp only [nhds_pi, Filter.mem_pi'] at hs

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s
⊢ ∃ I, I.piecewise x y ∈ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left✝ : ∀ x ∈ t, x ∈ s
hst : s ⊆ ↑t
⊢ s.Finite

Tactic:
exact t.finite_toSet.subset hst

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

Tactic:
refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint s t → Disjoint (↑(upperClosure s)) t
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = univ ↔ s = ⊥

Tactic:
simp [SetLike.ext'_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = ∅ ↔ s = ⊤

Tactic:
simp [SetLike.ext'_iff]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : x ∉ closure[inst✝²] {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x

Tactic:
exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inr.hs
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
this : x ∉ closure[inst✝²] {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}) x

Tactic:
exact continuousWithinAt_of_notMem_closure fun h =>
          this (closure_inter_subset_inter_closure _ _ h).2

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

pp: case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ContinuousOn f (s ∩ {a | p a})

pp: case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ContinuousOn g (s ∩ {a | ¬p a})

Tactic:
· rintro a ha
    simp only [hp a ha, ite_self]
    apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
    rcases ha with ⟨has, ⟨_, ha⟩⟩
    rw [← mem_compl_iff, ← closure_compl] at ha
    apply hg a ⟨has, ha⟩

Goal state after:
case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ContinuousOn f (s ∩ {a | p a})

case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst✝²] {a | p a})
hg : ContinuousOn g (s ∩ closure[inst✝²] {a | ¬p a})
⊢ ContinuousOn g (s ∩ {a | ¬p a})
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst✝, _] fun x ↦ x ∈ s
hs' : Continuous[inst✝, _] fun x ↦ x ∈ s'
x : α
hx : x ∉ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure[inst✝] tᶜ = s' ∩ closure[inst✝] tᶜ

Tactic:
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsDiscrete univ ↔ DiscreteTopology X

Tactic:
by
  simp [isDiscrete_iff_nhdsWithin, discreteTopology_iff_isOpen_singleton,
    isOpen_singleton_iff_nhds_eq_pure]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ⤳ x
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
simpa using hy.mem_open (hUo i) hi

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ Disjoint (𝓝 x) (𝓟 S)

Tactic:
simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hs : {x}.Subsingleton
⊢ IsClosed[inst✝¹] {x}

Tactic:
· exact isClosed_singleton

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ insert x s =ᶠ[𝓝 x] insert x t

Tactic:
by
  simp_rw [eventuallyEq_set] at h ⊢
  simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
    nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
    eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]
  filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)

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:
singleton_subset_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.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsPreirreducible S ↔ S.Subsingleton

Tactic:
simp [isPreirreducible_iff_forall_mem_subset_closure_singleton, Set.Subsingleton, eq_comm]

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

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

Tactic:
intro h
    filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
    simp_all [IsOpen.nhdsWithin_eq]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s ∈ cofinite
⊢ s ∈ codiscrete X

Tactic:
rw [← compl_compl s, compl_mem_codiscrete_iff]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s ∈ cofinite
⊢ IsClosed[inst✝¹] sᶜ ∧ IsDiscrete sᶜ
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen[inst✝¹] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen[inst✝¹] s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i),
    set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
⊢ IsPreconnected (K.pi fun i ↦ connectedComponentIn (t i) (x i))
Module: Mathlib.Topology.Connected.Clopen

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

Tactic:
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩

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

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
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
apply H

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ 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
⊢ IsPreconnected s

Tactic:
rw [isPreconnected_closed_iff]

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
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
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:
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.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
apply H

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst✝] (u ∩ s) →
    IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
subset_inter_iff

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 :
  IsClosed[inst✝] (u ∩ s) →
    IsClosed[inst✝] (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

Tactic:
refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩ <;> intro H u v hu hv hss huv
  · apply H u v hu hv hss
    rw [huv.inter_eq, inter_empty]
  have H1 := H (u ∩ s) (v ∩ s)
  rw [subset_inter_iff, subset_inter_iff] at H1
  simp only [Subset.refl, and_true] at H1
  apply H1 (hu.inter hs) (hv.inter hs)
  · rw [← union_inter_distrib_right]
    exact subset_inter hss Subset.rfl
  · rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected univ

Tactic:
← h (Classical.choice hα)

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
t' : β
ht' : t' ∈ T₁
⊢ {t'} ⊆ t

Tactic:
singleton_subset_iff

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
t' : β
ht' : t' ∈ T₁
⊢ t' ∈ t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
t' : β
ht' : t' ∈ T₂
⊢ {t'} ⊆ t

Tactic:
singleton_subset_iff

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
t' : β
ht' : t' ∈ T₂
⊢ t' ∈ t
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
exact (h x).anti (hs.subset_connectedComponent x_in)

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
by
  conv =>
    arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
  exact isOpen_iUnion fun a ↦ hs.preimage (by fun_prop) |>.inter <| ht.preimage (by fun_prop)

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
  rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
  use t, t_in, t_symm
  have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
  calc
    t ○ t ○ t ⊆ w ○ (t ○ t) := by gcongr
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Tactic:
exact ⟨fun h => h.congr_inseparable (hF.mono fun _ hx y _ => hx y),
    fun h => h.congr_inseparable (hF.mono fun _ hx y _ => (hx y).symm)⟩

Goal state after: