mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
have h₂₁ : x₂' < x₁ + p := toIcoMod_lt_right _ _ _

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ {x} ⊆ closure[inst✝] (id i')

Tactic:
id,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ (∀ s ∈ F, x ∈ closure[inst✝] s) ↔ ∀ i' ∈ F, ∃ i, True ∧ {x} ⊆ closure[inst✝] i'
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (closure[inst✝] t) s ↔ Disjoint s (closure[inst✝] t)

Tactic:
disjoint_comm

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint s (closure[inst✝] t) ↔ Disjoint s (closure[inst✝] t)
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
⊢ 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

Tactic:
simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)ᶜ

Tactic:
exact isOpen_induced h.isOpen_compl

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
s : Set X
hs : IsClosed[inst✝¹] s
h2s : s.Nonempty
⊢ IsClosed[inst✝] (f '' s)

Tactic:
· exact h s hs h2s

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), closure[inst✝] (f '' s) ⊆ f '' closure[inst✝¹] s
c : Set X
hc : IsClosed[inst✝¹] c
⊢ f '' closure[inst✝¹] c = f '' c

Tactic:
by rw [hc.closure_eq]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen[inst✝] U
V : Set X
hV : y ∈ V ∧ IsOpen[inst✝] V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
s : Set (CofiniteTopology X)
⊢ s.Nonempty → (WithTopology.ofTopology '' sᶜ).Finite ↔ s.Nonempty → sᶜ.Finite

Tactic:
finite_image_iff (WithTopology.ofTopology_injective _).injOn

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
by
  rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.1 h]
  · have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
    constructor
    · intro (H : IsOpen (s ×ˢ t))
      refine Or.inl ⟨?_, ?_⟩
      · simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
      · simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H
    · intro H
      simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
      exact H.1.prod H.2

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
s : Set α
hf : IsInducing f
⊢ ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s

Tactic:
by
  simp [ContinuousOn, ContinuousWithinAt, ← hf.map_nhdsWithin_eq]

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

Goal state before:
pp: case inl
α : Type u_2
x✝ : Bornology α
h : ∀ x ∈ ∅, IsBounded ∅
⊢ IsBounded ∅

pp: case inr
α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
x : α
hx : x ∈ s
⊢ IsBounded s

Tactic:
exacts [isBounded_empty, h x hx]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝¹ : (i : ι) → TopologicalSpace (B i)
inst✝ : Finite ι
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenEmbedding (f i)
⊢ IsOpen[Pi.topologicalSpace] (range (Pi.map f))

Tactic:
simpa using isOpen_set_pi Set.finite_univ fun i _ ↦ (hf i).2

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (univ.pi s)

Tactic:
classical
  rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
  · rw [he]
    exact countable_empty.isSeparable
  · choose c c_count hc using h
    have := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
⊢ IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] ((↑i).pi t)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun f hf => ?_

Goal state after:
case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
⊢ ∃ t_1 ⊆ (↑i).pi t, IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] t_1 ∧ f ∈ t_1
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
T : Set ↑I
hTc : T.Countable
hU : ⋃ i ∈ T, s ↑i = ⋃ i, s ↑i
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Tactic:
exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ⋂ i ∈ f u, i ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}

Tactic:
change IsOpen[generateFrom _] (⋂ i ∈ f u, i)

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] (⋂ i ∈ f u, i)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen[instTopologicalSpaceSum] ((fun u ↦ Sum.inl '' u) w)

Tactic:
exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)

Goal state after:
Module: Mathlib.Topology.Inseparable

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

Tactic:
exact ho.mem_nhds hxs

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : 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 (fun a ↦ if p a then f a else g a) s

Tactic:
apply ContinuousOn.if'
  · rintro a ha
    simp only [← hp a ha, ite_self]
    apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
    exact hf a ⟨ha.1, ha.2.1⟩
  · 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⟩
  · exact hf.mono (inter_subset_inter_right s subset_closure)
  · exact hg.mono (inter_subset_inter_right s subset_closure)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
Z : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : T2Space Z
s : Set X
t : Set Y
f g : X → Y → Z
h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y
hf₁ : ∀ (x : X), Continuous[inst✝², inst✝¹] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝³, inst✝¹] fun x ↦ f x y
hg₁ : ∀ (x : X), Continuous[inst✝², inst✝¹] (g x)
hg₂ : ∀ (y : Y), Continuous[inst✝³, inst✝¹] fun x ↦ g x y
this : closure[inst✝³] s ⊆ ⋂ y ∈ closure[inst✝²] t, {x | f x y = g x y}
⊢ ∀ x ∈ closure[inst✝³] s, ∀ y ∈ closure[inst✝²] t, f x y = g x y

Tactic:
by simpa only [subset_def, mem_iInter]

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

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Uf ∩ Ug = ∅
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
filter_upwards [inter_mem
      (hf.preimage_mem_nhds (IsOpen.mem_nhds h₁U h₃U))
      (hg.preimage_mem_nhds (IsOpen.mem_nhds h₂U h₄U))]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Uf ∩ Ug = ∅
⊢ ∀ a ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug, f a ≠ g a
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ interior s = s ↔ closure[inst✝] s ⊆ interior s

Tactic:
refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure[inst✝] s ⊆ interior s
⊢ closure[inst✝] s = s ∧ interior s = s
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝] (connectedComponentIn F y)

Tactic:
rw [← hf.isOpen_preimage, hf.continuous.continuousOn.preimage_connectedComponentIn]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LocallyConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsCoinducing f
F : Set β
hF : IsOpen[inst✝] F
y : β
x✝ : y ∈ F
⊢ IsOpen[inst✝²] (⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x)
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:
mem_image

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

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : ↑s → ↑s → Prop := ⋯
this : PreconnectedSpace ↑s
⊢ ∀ (x : { x // x ∈ s }), ∀ᶠ (y : { x // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x

Tactic:
rintro ⟨x, hx⟩
    have Z := h x hx
    rwa [nhdsWithin_eq_map_subtype_coe] at Z

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

Goal state before:
pp: α : 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)).Nonempty

Tactic:
by
    refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
    · simpa only [hsf, image_union] using image_mono (f := f) hsuv
    · simpa only [image_preimage_inter] using hsu.image f
    · simpa only [image_preimage_inter] using hsv.image f

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

Goal state before:
pp: case inl
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
c_count : ∅.Countable
c_cov : s ⊆ ⋃ i ∈ ∅, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
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]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
h : f ≤ 𝓟 s ∧ ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen[inst✝] i) ∧ iᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
choose fsub U hU hUf using h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : CountableInterFilter f
fsub : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
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 ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
hne : x ≠ y
this : Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)
⊢ Disjoint (𝓝 x) (𝓝 y)

Tactic:
exact this.elim id fun h => h.symm

Goal state after:
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:
rw [disjoint_left] at hUV ⊢

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.DenseEmbedding

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst✝¹] (f '' s i) ⊆ T
⊢ closure[inst✝¹] (f '' s i) ∈ 𝓝 (f x)

Tactic:
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure[inst✝¹] (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure[inst✝¹] (f '' s i) ∈ 𝓝 (f x)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
⊢ ∃ t, t.Countable ∧ ⋂ i ∈ t, C i = ⋂ i, C i

Tactic:
by
  conv in _ = _ => rw [← compl_inj_iff]; simp
  exact eq_open_union_countable (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

Goal state after:
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_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u

Tactic:
by
  refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩
  lift f to ℕ ≃ ℕ using hf
  simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

Tactic:
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ∀ l ≥ φ n, (u l, u <| φ n) ∈ V n⟩ :=
    extraction_forall_of_eventually' this

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
this : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : SetRel α α
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen[instTopologicalSpaceProd] u
hu₃ : u.IsSymm
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ (id V).preimage t

Tactic:
id,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ V.preimage t
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ ⊥.TotallyBounded

Tactic:
rw [← principal_empty, totallyBounded_principal_iff]
  exact totallyBounded_empty

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

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ ↑(setSeqAux hf U_mem N)

Tactic:
apply setSeq_sub_aux

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ ↑(setSeqAux hf U_mem N)

Tactic:
apply setSeq_sub_aux

Goal state after:
case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N