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

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst✝¹] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty

Tactic:
refine ⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst✝¹] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
⊢ f (invFun f (f x')) ∈ U
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, s x ⊆ ⋃ x, accumulate s x

Tactic:
· exact iUnion_mono fun i => subset_accumulate

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

Goal state before:
pp: case mk.mk
α : Type u_2
cobounded✝¹ : Filter α
le_cofinite✝¹ : cobounded✝¹ ≤ cofinite
cobounded✝ : Filter α
le_cofinite✝ : cobounded✝ ≤ cofinite
h_cobounded : cobounded α = cobounded α
⊢ { cobounded := cobounded✝¹, le_cofinite := le_cofinite✝¹ } = { cobounded := cobounded✝, le_cofinite := le_cofinite✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ Sum.inr '' closure[inst✝²] t = univ

Tactic:
htd.closure_eq,

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ Sum.inl '' univ ∪ Sum.inr '' univ = univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
⊢ ∀ (a : β) (u : Set β),
    a ∈ u → IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
intro a u ha hu

Goal state after:
case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
⊢ ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Filter α
h₁ : f.NeBot
h₂ : ∀ (g : Filter α), g.NeBot → g ≤ f → f ≤ g
g : Filter α
neBot'✝ : g.NeBot
le_of_le✝ : ∀ (g_1 : Filter α), g_1.NeBot → g_1 ≤ g → g ≤ g_1
x✝ : ↑{ toFilter := f, neBot' := h₁, le_of_le := h₂ } = ↑{ toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }
⊢ { toFilter := f, neBot' := h₁, le_of_le := h₂ } = { toFilter := g, neBot' := neBot'✝, le_of_le := le_of_le✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
s t : Set α
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Tactic:
simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α

Tactic:
refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α

Tactic:
by
  rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
  let := t.induced f
  refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
  rw [eq, induced_generateFrom_eq]

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

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ ⨅ s ∈ f, (𝓟 ∘ powerset) s = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
f : Filter α
⊢ ⨅ s ∈ f, 𝓟 (𝒫 s) = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
Module: Mathlib.Topology.Compactness.SigmaCompact

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

Tactic:
apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)

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

Goal state before:
pp: case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
⊢ ∀ (b : X (f k)), ∃ i i_1, ∃ (_ : i_1 ≤ i), ⟨f k, b⟩ ∈ Sigma.mk (f i_1) '' compactCovering (X (f i_1)) i

Tactic:
y

Goal state after:
case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
k : ℕ
y : X (f k)
⊢ ∃ i i_1, ∃ (_ : i_1 ≤ i), ⟨f k, y⟩ ∈ Sigma.mk (f i_1) '' compactCovering (X (f i_1)) i
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f.symm.symm '' s) = (UpperSet.map f.symm).symm (upperClosure s)

Tactic:
f.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
carrier✝¹ : Set α
upper'✝¹ : IsUpperSet carrier✝¹
carrier✝ : Set α
upper'✝ : IsUpperSet carrier✝
h : { carrier := carrier✝¹, upper' := upper'✝¹ }.carrier = { carrier := carrier✝, upper' := upper'✝ }.carrier
⊢ { carrier := carrier✝¹, upper' := upper'✝¹ } = { carrier := carrier✝, upper' := upper'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm.symm.symm b ∈ s

Tactic:
f.symm_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm b ∈ s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case hpf
α : 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 f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))

Tactic:
rintro a ha

Goal state after:
case hpf
α : 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 : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = sᶜ) → ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
exact fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩

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))

Tactic:
rintro a ha

Goal state after:
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 : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
⊢ ∀ ⦃b : Y⦄, flip (fun x1 x2 ↦ x1 ⤳ x2) b (f x) → ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = b

Tactic:
y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
y : Y
⊢ flip (fun x1 x2 ↦ x1 ⤳ x2) y (f x) → ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
⊢ ∀ ⦃b : Y⦄, (fun x1 x2 ↦ x1 ⤳ x2) b (f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = b

Tactic:
y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
⊢ (fun x1 x2 ↦ x1 ⤳ x2) y (f x) → ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y
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:
rw [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
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
⊢ ∀ ⦃y : X⦄, y ∈ s → x = y

Tactic:
y

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
⊢ y ∈ s → x = y
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 t ∩ (U \ s)).Finite

Tactic:
rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]
      simp

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

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
⊢ S ⊆ closure[inst✝¹] {x}

Tactic:
y

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
⊢ y ∈ S → y ∈ closure[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {x}

Tactic:
obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hs hx
  obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds
  grind

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
hs : ∀ i ∈ I, DiscreteTopology ↑(s i)
hs' : ∀ i ∈ I, IsClosed[inst✝] (s i)
⊢ DiscreteTopology ↑(⋃ i ∈ I, s i)

Tactic:
by
  simp only [← isDiscrete_iff_discreteTopology] at *
  exact .biUnion_finset hs hs'

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
inst✝ : Finite ι
s : ι → Set X
hs : ∀ (i : ι), DiscreteTopology ↑(s i)
hs' : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ DiscreteTopology ↑(⋃ i, s i)

Tactic:
by
  simp only [← isDiscrete_iff_discreteTopology] at *
  exact .iUnion hs hs'

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ IsCompact (closure[inst✝¹] K)

Tactic:
refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_
  rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩
  exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
x : X
hx : x ∈ K
⊢ ∀ x_1 ∈ L, ¬Inseparable x x_1

Tactic:
y

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
⊢ y ∈ L → ¬Inseparable x y
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False

Tactic:
exact mem_of_mem_nhds hd le_rfl

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

Goal state before:
pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Tactic:
simp only [IsBot, not_forall]
    rintro ⟨b, hb⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
    exact isClosed_Iic.isOpen_compl.mem_nhds hb

Goal state after:
Module: Mathlib.Topology.Clopen

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

Tactic:
· rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]

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

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X

Tactic:
apply R1Space.iInf

Goal state after:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ ∀ (i : Bool), R1Space X
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
⊢ ∀ y ∈ ⋃ n ∈ t, s n, ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
y

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
⊢ y ∈ ⋃ n ∈ t, s n → ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
hs : s ∈ compl '' S
⊢ s ∈ l

Tactic:
rw [mem_image] at hs

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
⊢ s ∈ l
Module: Mathlib.Topology.DenseEmbedding

Goal state before:

Tactic:
U ⊆ closure (i '' i ⁻¹' U) := di.dense.subset_closure_image_preimage_of_isOpen hUo
    _ ⊆ closure (i '' s) := closure_mono (image_mono sub)

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

Goal state before:
pp: case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : ⋃ i ∈ range k, U i = ⋃ i, U i
t_ne : (range k).Nonempty
⊢ ⋃ n, U (k n) = ⋃ i, U i

Tactic:
biUnion_range

Goal state after:
case h
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : ⋃ y, U (k y) = ⋃ i, U i
t_ne : (range k).Nonempty
⊢ ⋃ n, U (k n) = ⋃ i, U i
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ f, (∀ (n : ℕ), IsOpen[inst✝] (f n)) ∧ s = ⋂ n, f n) → IsGδ s
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
⊢ ∀ ⦃y : α⦄, y ∈ t → x = y

Tactic:
y

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
⊢ y ∈ t → x = y
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
⊢ IsNowhereDense (f '' t)

Tactic:
apply hf.isNowhereDense_image (isNowhereDense t tT)

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst✝] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
⊢ Dense (⋂ n, u n)

Tactic:
have := dense_iInter_of_isOpen_nat (fun n => hf.continuous.isOpen_preimage (u n) (hou n))
    (fun n => (IsOpenQuotientMap.dense_preimage_iff hf).mpr (hdu n))

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenQuotientMap f
u : ℕ → Set Y
hou : ∀ (n : ℕ), IsOpen[inst✝] (u n)
hdu : ∀ (n : ℕ), Dense (u n)
this : Dense (⋂ n, f ⁻¹' u n)
⊢ Dense (⋂ n, u n)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s ↦ s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s ↦ s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this :
  { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, uniformity := uniformity✝¹, symm := symm✝¹, comp := comp✝¹,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, uniformity := uniformity✝, symm := symm✝, comp := comp✝,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity✝ }

Tactic:
congr

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

Goal state before:
pp: case right
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (SetRel.symmetrize V) ⊆ s

Tactic:
exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub

Goal state after: