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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : ∃ I, I.Finite ∧ ∃ t_1, (∀ (i : ι), t_1 i ∈ 𝓝 (t i)) ∧ I.pi t_1 ⊆ n
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
obtain ⟨s, hs, n', hn', hsub⟩ := hn

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Goal state after:
Module: Mathlib.Topology.Piecewise

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

Tactic:
← inter_univ s,

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : {a | ∀ b ∈ t, (a, b) ∈ n} ∈ 𝓝ˢ[s'] s
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

Tactic:
exact ⟨_, hn, fun x hx ↦ hx.1 _ hx.2⟩

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'

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 ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ

Tactic:
apply ContinuousOn.if'

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

case hpg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ a ∈ univ ∩ frontier {a | p a}, Tendsto g (𝓝[univ ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

case hf
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn f (univ ∩ {a | p a})

case hg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn g (univ ∩ {a | ¬p a})
Module: Mathlib.Topology.Piecewise

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

Tactic:
by
  rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)

Tactic:
by
  convert! hf
  rw [cocompact_eq_cofinite X]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsClosed[inst✝] S ∧ IsDiscrete S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
rw [isDiscrete_iff_nhdsNE, isClosed_iff_clusterPt, ← forall_and]
  congrm (∀ x, ?_)
  rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]
  constructor <;> intro H
  · by_cases hx : x ∈ S
    exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]
  · refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
    simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

Goal state after:
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 : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ f ⁻¹' t ∈ irreducibleComponents Y

Tactic:
refine ⟨ht.1.preimage_of_isPreirreducible_fiber f hf₂ hf₃ h, fun u hu htu ↦ image_subset_iff.mp
    (subset_closure.trans (ht.2 (hu.image f hf₁.continuousOn).closure ?_))⟩
  suffices t ≤ closure (f '' f ⁻¹' t) from this.trans (closure_mono (image_mono htu))
  rw [image_preimage_eq_inter_range]
  exact subset_closure_inter_of_isPreirreducible_of_isOpen ht.1.2 hf₂.isOpen_range h

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

Goal state before:
pp: case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
H : IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Tactic:
exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsIrreducible S ↔ ∃ x, S = {x}

Tactic:
IsIrreducible,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ S.Nonempty ∧ IsPreirreducible S ↔ ∃ x, S = {x}
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a

Tactic:
by
  simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ⇨ t)

Tactic:
by
  simpa [himp_eq] using ht.union hs.compl

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ ContinuousOn f' (closure[inst✝²] {x | f x ≤ g x})

Tactic:
(isClosed_le hf hg).closure_eq

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderClosedTopology α
f g : β → α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst✝², inst✝⁵] f
hg : Continuous[inst✝², inst✝⁵] g
hf' : ContinuousOn f' {x | f x ≤ g x}
hg' : ContinuousOn g' {x | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ ContinuousOn f' {b | f b ≤ g b}
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
⊢ ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j

Tactic:
exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
      ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩

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

Goal state before:
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)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)

Tactic:
simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_closed j

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst✝] U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst✝] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst✝] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst✝] U
hUs : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ

Tactic:
exact
      ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsMeagre ∅

Tactic:
rw [IsMeagre, compl_empty]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ univ ∈ residual X
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ IsMeagre (s ∪ t)

Tactic:
rw [IsMeagre, compl_union]
  exact inter_mem hs ht

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
⊢ ¬IsMeagre s

Tactic:
by
  intro h
  obtain ⟨x, hx, hxc⟩ :=
    (dense_of_mem_residual (by rwa [IsMeagre] at h)).inter_open_nonempty s hs hne
  exact hxc hx

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

Goal state before:
pp: case inr.succ.succ.cons.refine_3
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
⊢ Pairwise (Disjoint on Fin.cons a (Fin.cons b U))

Tactic:
have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))

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

Goal state before:
pp: case inr.succ.succ
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
IH :
  ∃ U,
    (∀ (i : Fin (n + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
obtain ⟨U, h₁, h₂, h₃, h₄⟩ := IH
    obtain ⟨i, hi⟩ : ∃ i, ¬ IsConnected (U i) := by
      simp_rw [isConnected_iff_connectedSpace, ← not_forall]
      exact fun _ ↦ not_finite_iff_infinite.mpr ‹_› (.of_equiv _ (equivOfIsClopen h₁ h₃ h₄).symm)
    obtain ⟨U, rfl⟩ := (Equiv.piCongrLeft (fun _ ↦ Set α) (Equiv.swap 0 i)).symm.surjective U
    cases U using Fin.consCases with | cons s U =>
    simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
    obtain ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ := (show IsClopen s by simpa using h₁ i)
      |>.not_isPreconnected_iff.mp (mt (⟨by simpa using h₂ i, ·⟩) hi)
    refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))
    · have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))
    · simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
Cauchy,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α

Tactic:
rw [uniformity_eq_uniformity_interior]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ i, u i) = ⨅ i, comap f (u i)

Tactic:
by
  ext : 1
  simp [uniformity_comap, iInf_uniformity]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap (Prod.mk x) (𝓤 α)

Tactic:
← comap_map_mk_uniformity

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap (Prod.mk x) (Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)))
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
⊢ ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
have B : {z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
⊢ ∃ t, IsOpen[inst✝] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
a : α
⊢ (𝓝 a).IsCountablyGenerated

Tactic:
by rw [nhds_eq_comap_uniformity]; infer_instance

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

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
this : (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset
i : ι
hz : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
hi : i ∈ mulSupport fun i ↦ f i z
⊢ x ∈ U i

Tactic:
contrapose hz

Goal state after:
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
this : (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset
i : ι
hi : i ∈ mulSupport fun i ↦ f i z
hz : x ∉ U i
⊢ ¬(x ∉ U i → z ∈ (mulTSupport (f i))ᶜ)
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.RightInverse g ⇑f

Tactic:
convert! f.right_inv using 1

Goal state after: