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

Goal state before:
pp: case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] (eval i '' (↑I).pi fun a_1 ↦ ⋯.choose) ∧ a i ∈ eval i '' (↑I).pi fun a_1 ↦ ⋯.choose

Tactic:
eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)

Goal state after:
case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ⋯.choose ∧ a i ∈ ⋯.choose
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)

Tactic:
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun L ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id

Tactic:
hasBasis_self,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∀ t ∈ 𝓝ˢ K, ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ t
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬(𝓝[f i] x).NeBot
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
not_neBot

Goal state after:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
⊢ closure[inst✝] (⋃ i, f i) = ⋃ i, closure[inst✝] (f i)

Tactic:
ext x
  simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ⋃ x ∈ Finset.image Subtype.val t, U x ∈ 𝓝ˢ s

Tactic:
Finset.set_biUnion_finset_image

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ⋃ y ∈ t, U ↑y ∈ 𝓝ˢ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_2
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ (⋂₀ Q).Nonempty

Tactic:
replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
    exact hP hQP (hQ.image _)

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

Goal state before:
pp: case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) → ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
intro ⟨K, hK, hsK⟩ i

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki
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)
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE

Tactic:
tfae_have 1 → 4 := by
    simp only [continuous_def, CofiniteTopology.isOpen_iff']
    rintro H s (rfl | hs)
    · exact isOpen_empty
    · rw [← compl_compl s, preimage_compl]
      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl

Goal state after:
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
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
⊢ (f ⁻¹' Z).Nonempty

Tactic:
obtain ⟨x, hx⟩ := hV.1.1

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
intro h z h₁z
    obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
    use t \ (t ∩ (U \ s)), nhdsNE_of_nhdsNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) h₂t
    simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ ContinuousOn f s

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)
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_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = ∅
⊢ False

pp: case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ False

Tactic:
· exact (h_nonempty i).ne_empty hi

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (tᶜ ∩ t'ᶜ)).Nonempty
⊢ False

Tactic:
← compl_union

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
t t' : Set α
ht : IsClosed[inst✝] t
ht' : IsClosed[inst✝] t'
htt' : s ⊆ t ∪ t'
x : α
xs : x ∈ s
xt : x ∈ t
y : α
ys : y ∈ s
yt' : y ∈ t'
h' : s ⊆ tᶜ ∪ t'ᶜ
xt' : x ∉ t'
yt : y ∉ t
this : (s ∩ (t ∪ t')ᶜ).Nonempty
⊢ False
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
← disjoint_principal_right,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ Disjoint (𝓝 x ⊓ f) (𝓟 s)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
this : (s ∩ (uᶜ ∩ vᶜ)).Nonempty
⊢ False

Tactic:
← compl_union

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
h' : s ⊆ uᶜ ∪ vᶜ
xv : x ∉ v
yu : y ∉ u
this : (s ∩ (u ∪ v)ᶜ).Nonempty
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst✝] u
hu' : IsOpen[inst✝¹] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst✝] v
hv' : IsOpen[inst✝¹] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty

Tactic:
rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with
    ⟨_, ⟨z, hzs, rfl⟩, hzuv⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
h : IsPreconnected (f '' s)
x : α
hxs : x ∈ s
y : α
hys : y ∈ s
u : Set β
hu : IsOpen[inst✝] u
hu' : IsOpen[inst✝¹] (f ⁻¹' u)
hxu : x ∈ f ⁻¹' u
v : Set β
hv : IsOpen[inst✝] v
hv' : IsOpen[inst✝¹] (f ⁻¹' v)
hyv : y ∈ f ⁻¹' v
huv : f '' s ⊆ u ∪ v
z : α
hzs : z ∈ s
hzuv : f z ∈ u ∩ v
⊢ (s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : IsInducing f
⊢ IsPreconnected (f '' s) ↔ IsPreconnected s

Tactic:
refine ⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩
  rintro u v hu' hv' huv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩
  rcases hf.isOpen_iff.1 hu' with ⟨u, hu, rfl⟩
  rcases hf.isOpen_iff.1 hv' with ⟨v, hv, rfl⟩
  replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]
  rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with
    ⟨_, ⟨z, hzs, rfl⟩, hzuv⟩
  exact ⟨z, hzs, hzuv⟩

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun L ↦ L ∈ 𝓝ˢ K ∧ IsCompact L ∧ IsClosed[inst✝²] L) id

Tactic:
hasBasis_self,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ ∀ t ∈ 𝓝ˢ K, ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2.a
α : 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 ⊆ v
⊢ s ⊆ u ∩ s ∪ v ∩ s

Tactic:
rw [← union_inter_distrib_right]
    exact subset_inter hss Subset.rfl

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ

Tactic:
obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : LindelofSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Set X
tc : t.Countable
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, U x = univ
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst✝ : TopologicalSpace X
⊢ CountableInterFilter (residual X)

Tactic:
rw [residual]; infer_instance

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ interior (closure[inst✝] ∅) = ∅

Tactic:
closure_empty,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ interior ∅ = ∅
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ interior s = ∅ ↔ IsClosed[inst✝] s ∧ Dense sᶜ

Tactic:
interior_eq_empty_iff_dense_compl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ Dense sᶜ ↔ IsClosed[inst✝] s ∧ Dense sᶜ
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : s = ∅
⊢ IsMeagre s

Tactic:
simpa [hs] using IsMeagre.empty

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

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ a

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
        from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
      · apply Subset.trans _ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst✝¹] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
⊢ Dense (⋂₀ S)

Tactic:
rcases hS.exists_eq_range h with ⟨f, rfl⟩
    exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h : IsMeagre s
⊢ ?m.17 ∈ residual X

Tactic:
rwa [IsMeagre] at h

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Nonempty X
s : Set X
hs : s ∈ residual X
⊢ ¬IsMeagre s

Tactic:
by
  rcases (mem_residual (X := X)).1 hs with ⟨t, ht_sub, htGδ, ht_dense⟩
  intro hs_meagre
  exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
hs : IsPreconnected (⇑h '' s)
⊢ IsPreconnected s

Tactic:
simpa only [image_symm, preimage_image]
    using hs.image _ h.symm.continuous.continuousOn

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
⊢ (f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s) ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, forall_mem_comm]

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

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

Tactic:
rw [map_swap_eq_comap_swap]; exact tendsto_swap_uniformity.le_comap

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
by
  let cl_d := { p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }
  have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
    mem_nhds_iff.mp <|
      show cl_d ∈ 𝓝 (x, y) by
        rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
  choose t ht using this
  exact ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : SetRel α α),
    isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left,
    fun ⟨a, b⟩ hp => by
      simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
    iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]
  constructor
  · rintro ⟨V, V_in, V_sub⟩
    use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance
    exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub
  · rintro ⟨V, V_in, _, V_sub⟩
    exact ⟨V, V_in, V_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 ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2))
    ((p ×ˢ q) ×ˢ p' ×ˢ q') (𝓤 β ×ˢ 𝓤 β')

Tactic:
← map_swap4_prod,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun q ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2))
    (map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((p ×ˢ p') ×ˢ q ×ˢ q')) (𝓤 β ×ˢ 𝓤 β')
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Tactic:
rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ (𝓤 β).lift' ((fun s ↦ s ○ s) ∘ preimage fun p ↦ (f p.1, f p.2)) ≤
    UniformSpace.uniformity.lift' ((preimage fun p ↦ (f p.1, f p.2)) ∘ fun s ↦ s ○ s)

pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone fun s ↦ s ○ s

Tactic:
· exact lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone fun s ↦ s ○ s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
s : Set α
inst✝ : UniformSpace α
⊢ map (Prod.map Subtype.val Subtype.val) (comap (Prod.map Subtype.val Subtype.val) (𝓤 α)) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Tactic:
map_comap,

Goal state after:
α : Type ua
s : Set α
inst✝ : UniformSpace α
⊢ 𝓤 α ⊓ 𝓟 (range (Prod.map Subtype.val Subtype.val)) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.domRestrict f)
⊢ ContinuousOn f s

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.domRestrict f)
⊢ Continuous[instTopologicalSpaceSubtype, inst✝.toTopologicalSpace] (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: case mk
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x✝ : SeparationQuotient α
a : α
⊢ map f (Quot.mk (⇑(inseparableSetoid α)) a) = g (Quot.mk (⇑(inseparableSetoid α)) a)

Tactic:
calc
    map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
    _ = g ⟦a⟧ := congr_fun comm a

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ comap (fun x ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α

Tactic:
by rw [← Prod.map_def, Prod.map_id, comap_id]

Goal state after: