mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (K.1 ×ˢ K.2)ᶜ ∈ cocompact (X × Y)

Tactic:
exact (hK.1.prod hK.2).compl_mem_cocompact

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

Goal state before:
pp: case h
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
hcne : ¬c.Nonempty
⊢ Sᶜᶜ.Nonempty

Tactic:
compl_compl

Goal state after:
case h
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
hcne : ¬c.Nonempty
⊢ S.Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ x ∈ t, IsClosed[inst✝] ((Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) x)) →
      s ⊆ ⋃₀ ↑(Finset.map (Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) t) →
        ∃ z, (∃ a ∈ t, (Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) a = z) ∧ s ⊆ z

Tactic:
Finset.coe_map,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ x ∈ t, IsClosed[inst✝] ((Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) x)) →
      s ⊆ ⋃₀ (⇑(Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) '' ↑t) →
        ∃ z, (∃ a ∈ t, (Equiv.toEmbedding (Function.Involutive.toPerm compl ⋯)) a = z) ∧ s ⊆ z
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}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = V'ᶜᶜ

Tactic:
compl_compl

Goal state after:
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}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = V'
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ (f ⁻¹' t).Nonempty

Tactic:
obtain ⟨-, hx, x, rfl⟩ := h

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
x : Y
hx : f x ∈ t
⊢ (f ⁻¹' t).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
⊢ (∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ∧ (x ∈ s → ContinuousWithinAt (update f x y) s x) ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))

Tactic:
refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b
z : X
hz : z ∈ s \ {x}
⊢ ContinuousWithinAt f (s \ {x}) z

case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
H : ContinuousOn f (s \ {x})
z : X
hzx : z ≠ x
hzs : z ∈ s
⊢ ContinuousWithinAt (update f x y) s z

case refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
x✝ : x ∈ s
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ ↑t)

Tactic:
induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← sdiff_sdiff]
    exact ih.sdiff_singleton _

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

Goal state before:
pp: case mp
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 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

Tactic:
intro h
    filter_upwards [h] with _ hy
    exact eventually_nhdsWithin_of_eventually_nhds hy

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 : ∀ (x : X), ¬AccPt x (𝓟 Sᶜᶜ)
⊢ False

Tactic:
compl_compl

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.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, x ∈ s_1

Tactic:
rintro r (rfl | rfl | h) <;> assumption

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ s_1 ∈ {s, t}, IsPreconnected s_1

Tactic:
rintro r (rfl | rfl | h) <;> assumption

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X = cocompact X

Tactic:
refine le_antisymm ?_ cocompact_le_coclosedCompact
  rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]
  exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

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 : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
have := hS.toEncodable

Goal state after:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
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
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Tactic:
have := hS.toEncodable

Goal state after:
α : 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
this : Encodable ↑S
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
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
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Tactic:
have := hS.toEncodable

Goal state after:
α : 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
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
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
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (f ⁻¹' u ∪ f ⁻¹' v) ∩ s
⊢ s ⊆ u' ∪ v'

Tactic:
rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv

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
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ (u' ∪ v') ∩ s
⊢ s ⊆ u' ∪ v'
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
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [hsf, image_union] using image_mono (f := f) hsuv

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ s ⊆ f '' u ∪ f '' v

pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [hsf, image_union] using image_mono (f := f) hsuv

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' u).Nonempty

case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
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
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

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) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
· apply H u v hu hv hss
    rw [huv.inter_eq, inter_empty]

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) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
⊢ Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)

Tactic:
disjoint_left

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
⊢ ∀ ⦃a : { x // x ∈ e }⦄, a ∈ Subtype.val ⁻¹' closure[inst✝] s → a ∉ Subtype.val ⁻¹' closure[inst✝] t
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ Disjoint (U ∩ e) (V ∩ e)

Tactic:
disjoint_left

Goal state after:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : ∀ ⦃a : { x // x ∈ e }⦄, a ∈ Subtype.val ⁻¹' U → a ∉ Subtype.val ⁻¹' V
⊢ ∀ ⦃a : X⦄, a ∈ U ∩ e → a ∉ V ∩ e
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case connected_fibers
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : β
⊢ ∀ (t : β), IsConnected (f ⁻¹' {t})

Tactic:
exact connected_fibers

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
⊢ (∀ (i : Fin (0 + 1)), IsClopen (![univ] i)) ∧
    (∀ (i : Fin (0 + 1)), (![univ] i).Nonempty) ∧ Pairwise (Disjoint on ![univ]) ∧ ⋃ i, ![univ] i = univ

Tactic:
simp [isClopen_univ, Set.iUnion_fin_add_one_eq_iUnion_succ]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen[inst✝.toTopologicalSpace] s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Tactic:
simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prodMk]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
exact tendsto_swap_uniformity.le_comap

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (𝓤 α).sets

Tactic:
← comap_swap_uniformity

Goal state after:
α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
intro V

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
⊢ V ∈ 𝓤 α → ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α

Tactic:
intro V

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
⊢ V ∈ 𝓤 α → V ∈ 𝓝 (x, x)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
t : Set α
⊢ t ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓤 α ∧ i.IsSymm) ∧ ball x i ⊆ t

Tactic:
by simp [UniformSpace.mem_nhds_iff_symm, and_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (comap (Prod.mk c) (𝓤 β)) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'

Tactic:
tendsto_comap_iff

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun x ↦ c) p p'
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s
⊢ (s.symmetrize ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s.symmetrize) ∧ s.symmetrize.IsSymm ∧ id s.symmetrize ⊆ id s

Tactic:
exact
    ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
      inferInstance, SetRel.symmetrize_subset_self⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V

Tactic:
intro V

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
⊢ V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (comap (Prod.mk a) (𝓤 α)) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)

Tactic:
tendsto_comap_iff

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x ↦ (a, u x)) f (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (comap (fun y ↦ (y, a)) (𝓤 α)) ↔ Tendsto (fun x ↦ (u x, a)) f (𝓤 α)

Tactic:
tendsto_comap_iff

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y ↦ (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x ↦ (u x, a)) f (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α✝ : Type u
β : Type v
uniformSpace : UniformSpace α✝
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
f✝ : Filter α
hf : Cauchy f✝
⊢ ∃ x, f✝ ≤ 𝓝 x

Tactic:
by simpa using (isCompact_iff_totallyBounded_isComplete.1 isCompact_univ).2 _ hf

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

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
⊢ CompactSpace γ

Tactic:
rwa [h]

Goal state after:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen[inst✝³] U
f : ↑U → β
cont : Continuous[instTopologicalSpaceSubtype, inst✝] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt (extend Subtype.val f 1 ∘ Subtype.val) ⟨x, ⋯⟩

Tactic:
extend_comp Subtype.val_injective

Goal state after:
α' : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : T2Space α'
inst✝ : TopologicalSpace β
U : Set α'
hU : IsOpen[inst✝³] U
f : ↑U → β
cont : Continuous[instTopologicalSpaceSubtype, inst✝] f
supp : HasCompactMulSupport f
x : α'
h : x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContinuousAt f ⟨x, ⋯⟩
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Goal state after: