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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B

Tactic:
sUnion_eq_univ_iff

Goal state after:
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
⊢ {x} ∈ B
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
nhds_pi

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi s ∈ 𝓝 x

Tactic:
by
  rw [pi_def, biInter_mem hi]
  exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ IsSeparable s ↔ SeparableSpace α

Tactic:
simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]

Goal state after:
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 β
ha : a ∈ u
hu : IsOpen[⨅ i, t i] u
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩

Goal state after:
case refine_2.refine_1
β : 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
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ hF.toFinset, U i ∈ T i

case refine_2.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
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ a ∈ ⋂ i ∈ hF.toFinset, U i

case refine_2.refine_3
β : 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
F : Set ι
U : ι → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ hF.toFinset, U i ⊆ u
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), FirstCountableTopology (X i)
f : (i : ι) → X i
⊢ (𝓝 f).IsCountablyGenerated

Tactic:
nhds_pi

Goal state after:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), FirstCountableTopology (X i)
f : (i : ι) → X i
⊢ (Filter.pi fun i ↦ 𝓝 (f i)).IsCountablyGenerated
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen[coinduced (⇑Equiv.ulift.symm) inst✝] s ↔ IsOpen[inst✝] (up ⁻¹' s)

Tactic:
← isOpen_coinduced

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsOpen[coinduced (⇑Equiv.ulift.symm) inst✝] s ↔ IsOpen[coinduced up inst✝] s
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
⊢ IsOpen[t✝] v → ∃ v_1 ∈ ⋃ u ∈ countableBasis α, s u, x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
hv

Goal state after:
case h_nhds
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : Set α → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t✝] v
⊢ ∃ v_1 ∈ ⋃ u ∈ countableBasis α, s u, x ∈ v_1 ∧ v_1 ⊆ v
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la

Tactic:
eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la
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 α) := (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'
v : Set α
⊢ v ∈ f u → v ∈ {s | IsOpen[ts] s}

Tactic:
hv

Goal state after:
case refine_2.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'
v : Set α
hv : v ∈ f u
⊢ v ∈ {s | IsOpen[ts] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h_open
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∀ u ∈ image π '' V, IsOpen[inst✝] u

Tactic:
rintro - ⟨U, U_in_V, rfl⟩
    apply h U (hV.isOpen U_in_V)

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

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
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : ⋃ x ∈ s, K x = univ
⊢ ⋃₀ (K '' s) = univ

Tactic:
sUnion_image

Goal state after:
X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s✝ t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
K : X → Set X
hKc : ∀ (x : X), IsCompact (K x)
hxK : ∀ (x : X), K x ∈ 𝓝 x
s : Set X
hsc : s.Countable
hsU : ⋃ x ∈ s, K x = univ
⊢ ⋃ a ∈ s, K a = univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
by
  rw [← nhdsSet_singleton]
  exact hs.le_nhdsSet_of_clusterPt hmem h

Goal state after:
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
w✝ : { x // x ∈ β }
ha : w✝ ∈ γ
⊢ ⟨↑w✝, ⋯⟩ ∈ γ

Tactic:
exact ha

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃₀ (preimage Subtype.val '' S)

Tactic:
sUnion_image

Goal state after:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃ a ∈ S, A ↓∩ a
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}
⊢ [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 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff

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}
⊢ [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.Separation.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun x y ↦ ∃ U, IsOpen[inst✝] U ∧ Xor (x ∈ U) (y ∈ U)

Tactic:
simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
    inseparable_iff_forall_isOpen, Pairwise]

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
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
⊢ (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
hv

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
⊢ u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen[inst✝] u
⊢ IsOpen[inst✝] v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hv

Goal state after:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
⊢ T2Space ((i : ι) × X i)

Tactic:
constructor
  rintro ⟨i, x⟩ ⟨j, y⟩ ne
  rcases eq_or_ne i j with (rfl | h)
  · replace ne : x ≠ y := ne_of_apply_ne _ ne
    exact separated_by_isOpenEmbedding .sigmaMk ne
  · let _ := (⊥ : TopologicalSpace ι); have : DiscreteTopology ι := ⟨rfl⟩
    exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

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

Goal state before:
pp: case mpr
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 : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ f x ≠ g x

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg
    exact h₁t x h₃t

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
u v : Set X
hu : IsOpen[inst✝¹] u
⊢ IsOpen[inst✝¹] v → (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty

Tactic:
hv

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}
u v : Set X
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
⊢ (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a

Tactic:
continuousWithinAt_Iio_iff_Iic,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsLT h]

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
⊢ IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
hv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
⊢ s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
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
⊢ IsOpen[inst✝] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hv

Goal state after:
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
⊢ s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case sUnion
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t✝ : Set X
S : Set (Set X)
a✝ : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, a ∈ s → Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)

Tactic:
grw [compl_sUnion, sInter_image, iInter₂_subset t ht]

Goal state after:
case sUnion
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t✝ : Set X
S : Set (Set X)
a✝ : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, a ∈ s → Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ ∃ V, IsOpen[inst✝¹] V ∧ K ⊆ V ∧ closure[inst✝¹] V ⊆ U

Tactic:
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
    simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using! hU

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
⊢ ∃ V, IsOpen[inst✝¹] V ∧ K ⊆ V ∧ closure[inst✝¹] V ⊆ U
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst✝] u
⊢ IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
hv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
⊢ s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: 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 : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → ↑c
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
n : ℕ
hn : f n = ⟨x, hx⟩
⊢ U x = U ↑(f n)

Tactic:
rw [hn]

Goal state after:
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
⊢ IsClosed[inst✝] v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
hv

Goal state after:
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
⊢ s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
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
⊢ IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

Tactic:
hv

Goal state after:
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
⊢ s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
⊢ IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
hv

Goal state after:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed[inst✝] s
H : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
⊢ s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
⊢ IsClosed[inst✝¹] v → f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
hv

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
⊢ f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s

Tactic:
exact ⟨a, ha⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
⊢ φ ⁻¹' V' ∈ 𝓝 b

Tactic:
set V₁ := { x | Tendsto f (comap i <| 𝓝 x) (𝓝 <| φ x) }

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ φ ⁻¹' V' ∈ 𝓝 b
Module: Mathlib.Topology.Connected.TotallyDisconnected

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

Tactic:
by
  refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
  obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩
  rw [hf.isInducing.isPreconnected_image] at hu
  exact (hs v hvs hu).image _

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

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄, x ≠ y → ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
refine forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case refine_1
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ u v, IsOpen[inst✝] u ∧ IsOpen[inst✝] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

Tactic:
exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩

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

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq fun n ↦ u (n + k)
⊢ CauchySeq u

pp: case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n ↦ u (n + k)

Tactic:
· rw [cauchySeq_iff] at h ⊢
    intro V mV
    obtain ⟨N, h⟩ := h V mV
    use N + k
    intro a ha b hb
    convert! h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> lia

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq fun n ↦ u (n + k)