mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
rw [range_comp]

Goal state after:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
is : Set β
P : β → α → Prop
his : is.Finite
⊢ (∀ᶠ (i : α) in ↑f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in ↑f, P a i

Tactic:
simp only [Filter.Eventually, Ultrafilter.mem_coe]
  convert! f.finite_biUnion_mem_iff his (s := P) with i
  aesop

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
⊢ ∀ (i' : ℕ), True → b x i' ∈ 𝓝 x

Tactic:
intro n

Goal state after:
case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
n : ℕ
⊢ True → b x n ∈ 𝓝 x
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
⊢ SecondCountableTopology α

Tactic:
let := t.induced f

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
⊢ SecondCountableTopology α
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
forall_prod_set,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
⊢ (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 (x, y), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ px,
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
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
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_generateFrom_iff_subset_isOpen.2
      simp only [iUnion_subset_iff]
      intro u hu v hv
      rw [ht]
      apply isOpen_generateFrom_of_mem
      exact ft u hu hv

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
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
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)

pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
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
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts

Tactic:
· apply le_generateFrom_iff_subset_isOpen.2
      simp only [iUnion_subset_iff]
      intro u hu v hv
      rw [ht]
      apply isOpen_generateFrom_of_mem
      exact ft u hu hv

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
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
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
⊢ LocallyCompactSpace X

Tactic:
refine .of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
x✝ : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left✝ : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (f ⁻¹' (s ∩ Z))
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case mpr.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ f ⁻¹' L n ∩ s) n)

Tactic:
intro n

Goal state after:
case mpr.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ IsCompact ((fun n ↦ f ⁻¹' L n ∩ s) n)
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
exact ⟨Set.image π '' V, V_countable.image (Set.image π),
      (V_generates.isQuotientMap h' h).eq_generateFrom⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
hnf : f.NeBot
⊢ f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
hstf

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
by
  refine (forall_neBot_le_iff ?_).trans ?_
  · rintro f g hle ⟨x, hxs, hxf⟩
    exact ⟨x, hxs, hxf.mono hle⟩
  · simp only [Ultrafilter.clusterPt_iff]

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

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

Tactic:
intro H
    choose K hK hsK using H
    exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
⊢ closure[inst✝¹] {x} = (𝓝 x).ker

Tactic:
by
  ext; simp [ker_nhds_eq_specializes, ← specializes_iff_mem_closure, specializes_comm]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : PreirreducibleSpace ↑s
⊢ IsPreirreducible s

Tactic:
rw [← Subtype.range_coe (s := s), ← Set.image_univ]
  refine PreirreducibleSpace.isPreirreducible_univ.image Subtype.val ?_
  exact continuous_subtype_val.continuousOn

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 : IsIrreducible t
f : Y → X
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
⊢ IsIrreducible (f ⁻¹' t)

Tactic:
refine ⟨?_, IsPreirreducible.preimage_of_isPreirreducible_fiber ht.2 f hf₂ hf₃⟩
  obtain ⟨-, hx, x, rfl⟩ := h
  exact ⟨x, hx⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst✝²] s
x : X
hx : x ∈ t
⊢ f x = g x

Tactic:
have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
s t : Set X
f g : X → Y
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure[inst✝²] s
x : X
hx : x ∈ t
this : (𝓝[s] x).NeBot
⊢ f x = g x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), R1Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact (closure[topologicalSpace] s) ↔ ∀ (i : ι), IsCompact (closure[inst✝¹ i] (eval i '' s))

Tactic:
← exists_isCompact_superset_iff,

Goal state after:
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), R1Space (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ K, IsCompact K ∧ eval i '' s ⊆ K
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst✝²] s
ht : ∀ y ∈ s, f y = c
⊢ f x ∈ closure[inst✝¹] {c}

Tactic:
exact h.mem_closure hx ht

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 : ι), IsClosed[inst✝¹] (s i)
hs : ∀ (i : ι), IsDiscrete (s i)
⊢ IsDiscrete (⋃ i, s i)

Tactic:
exact .iUnion hs hs'

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ a ∈ upperBounds (closure[inst✝²] s) ↔ a ∈ upperBounds s

Tactic:
mem_upperBounds_iff_subset_Iic,

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ closure[inst✝²] s ⊆ Iic a ↔ s ⊆ Iic a
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)

Tactic:
rcases H with ⟨x, hxs, hxt⟩
  exact hs.union x hxs hxt ht

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
rw [locallyConnectedSpace_iff_connected_subsets]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ LocallyConnectedSpace (α × β)

Tactic:
rw [locallyConnectedSpace_iff_connected_subsets]

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝³ : TopologicalSpace α
s t u v : Set α
inst✝² : TopologicalSpace β
inst✝¹ : LocallyConnectedSpace α
inst✝ : LocallyConnectedSpace β
⊢ ∀ (x : α × β), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
· rw [piecewise_eq_of_notMem _ _ _ hi]
    have : PreconnectedSpace (X i) := not_not.mp (not_or.1 hi).2
    exact isPreconnected_univ

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t

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

Goal state before:
pp: α : 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)
⊢ ¬Nontrivial ι

Tactic:
by_contra ⟨i, j, h_ne⟩

Goal state after:
α : 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 : i ≠ j
⊢ False
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
⊢ f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
hstf

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst✝¹] t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsConnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

Tactic:
IsConnected,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ s.Nonempty ∧ IsPreconnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
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
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
h : s ⊆ u ∨ s ⊆ v
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsConnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty

Tactic:
IsConnected,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (connectedComponentIn F x).Nonempty ∧ IsPreconnected (connectedComponentIn F x) ↔ (connectedComponentIn F x).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ (s ∩ (a ∩ b)).Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
⊢ s ∩ (a ∩ b) ≠ ∅
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ t ⊆ (closure[inst✝²] s)ᶜ

Tactic:
subset_compl_iff_disjoint_left

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyNormalSpace Y
e : X → Y
he : IsInducing e
s t : Set X
hd₁ : Disjoint (closure[inst✝²] s) t
hd₂ : Disjoint s (closure[inst✝²] t)
⊢ Disjoint (closure[inst✝²] s) t
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst✝², inst✝] f
⊢ ConnectedSpace β

Tactic:
rw [connectedSpace_iff_univ, ← hf.range_eq]

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous[inst✝², inst✝] f
⊢ IsConnected (range f)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ closure[inst✝] (i '' s) ∈ 𝓝 (i a)

Tactic:
by
  rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
  rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
  refine mem_of_superset (hUo.mem_nhds haU) ?_
  calc
    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.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : closure[inst✝¹] (i '' s) ∈ 𝓝 (i x)
⊢ False

Tactic:
rw [(hs.image di.continuous).isClosed.closure_eq] at this

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ IsConnected univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
IsConnected,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ univ.Nonempty ∧ IsPreconnected univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
← tendstoUniformlyOn_univ,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOnFilter F f p ⊤
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p

Tactic:
← tendstoUniformlyOn_univ,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F' f p
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:
← tendstoUniformlyOn_univ,

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
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ f✝ ≤ 𝓝 (x1, x2)

Tactic:
rw [nhds_prod_eq, le_prod]; constructor <;> assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i

Tactic:
← tendstoUniformlyOn_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ (𝓟 ∅).TotallyBounded

Tactic:
totallyBounded_principal_iff

Goal state after:
α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded ∅