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
a b : α
⊢ [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE

Tactic:
rw [modEq_iff_toIcoMod_eq_left hp]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
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₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
hequiv : x₃' ≤ toIocMod hp x₂' x₁
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
    simpa [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_right]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C

Tactic:
accPt_iff_frequently,

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
⊢ (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot

Tactic:
rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ (F.lift' closure[inst✝] ⊓ pure x).NeBot

Tactic:
rw [clusterPt_iff_lift'_closure, inf_comm]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] ↔ (pure x ⊓ F.lift' closure[inst✝]).NeBot
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
a : α
⊢ ⋃ n, Ico (a + ↑n) (a + ↑n + 1) = univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    iUnion_Ico_add_zsmul zero_lt_one a

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ

Tactic:
by rw [Set.inter_comm]; exact h.nhdsSet_le_sup s

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
x : X
y : Y
hs : Prod.fst ⁻¹' s ∈ 𝓝 (x, y) ⊓ 𝓟 (Prod.snd ⁻¹' {(x, y).2})
⊢ s ∈ 𝓝 (x, y).1

Tactic:
mem_inf_principal,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s} ∈ 𝓝 (x, y)
⊢ s ∈ 𝓝 (x, y).1
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : Prod.snd ⁻¹' s ∈ 𝓝 (x, y) ⊓ 𝓟 (Prod.fst ⁻¹' {(x, y).1})
⊢ s ∈ 𝓝 (x, y).2

Tactic:
mem_inf_principal,

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
hs : {x_1 | x_1 ∈ Prod.fst ⁻¹' {(x, y).1} → x_1 ∈ Prod.snd ⁻¹' s} ∈ 𝓝 (x, y)
⊢ s ∈ 𝓝 (x, y).2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing fun x ↦ (f x, y)) ↔ IsInducing f

Tactic:
simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)

Tactic:
by
  rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ s = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Tactic:
refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s} ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ IsTopologicalBasis s

Tactic:
by
  convert! isTopologicalBasis_of_subbasis hsg
  refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_
  rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩
  lift g to Finset (Set α) using hg
  exact hsi.finiteInter_mem g hgs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t) ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t

Tactic:
← closure_eq_iff_isClosed,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ closure[instTopologicalSpaceSubtype] (s ↓∩ t) = s ↓∩ t ↔ s ∩ closure[inst✝] (s ∩ t) ⊆ t
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s t : Set α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

Goal state after:
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ (𝓝 x ⊓ f).NeBot ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x

Tactic:
← le_inf_iff,

Goal state after:
X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ (𝓝 x ⊓ f).NeBot ↔ ∃ u, ↑u ≤ f ⊓ 𝓝 x
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ U, ↑U ≤ F ∧ ↑U ≤ comap u (𝓝 x)

Tactic:
← le_inf_iff,

Goal state after:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ U, ↑U ≤ F ⊓ comap u (𝓝 x)
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:
by rw [nhds_pi]; infer_instance

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
h : IsInducing f
i : ι
U : Set X
hUo : IsOpen[inst✝] U
hU : f ⁻¹' U = range (Sigma.mk i)
⊢ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i

Tactic:
simpa [Set.ext_iff] using hU

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

Goal state before:
pp: α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ i, p i ∧ q (s i)

Tactic:
rw [l.eventually_smallSets' hq, hl.exists_iff hq]

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ {i | (f i).Nonempty}.Finite

Tactic:
by
  simpa only [inter_univ] using hf.finite_nonempty_inter_compact isCompact_univ

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
⊢ IsCompact (f '' s)

Tactic:
intro l

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
⊢ ∀ [l.NeBot], l ≤ 𝓟 (f '' s) → ∃ x ∈ f '' s, ClusterPt x l
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
· rcases exists_surjective_nat ι with ⟨f, hf⟩
    refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
    · refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
      exact (isCompact_compactCovering _ _).image continuous_sigmaMk
    · simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
      intro k y
      rcases exists_mem_compactCovering y with ⟨n, hn⟩
      refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
      exact compactCovering_subset _ (le_max_right _ _) hn

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst✝] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
⊢ ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F

Tactic:
simpa [nhds_generateFrom] using hF

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t

Tactic:
exact fun h a b hb hba ha ↦ h hb <| ht hba ha

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
⊢ IsCompact (insert y (range f))

Tactic:
intro l

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
⊢ ∀ [l.NeBot], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)

Tactic:
by
  apply le_antisymm
  · exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)
  · refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_
    rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]
    exact (hK.1.prod hK.2).compl_mem_cocompact

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set Y
⊢ DiscreteTopology ↑s ↔ ∀ y ∈ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = {y}

Tactic:
discreteTopology_subtype_iff'

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set Y
⊢ (∀ y ∈ s, ∃ U, IsOpen[inst✝] U ∧ U ∩ s = {y}) ↔ ∀ y ∈ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = {y}
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ IsClosed[inst✝] s

Tactic:
← closure_eq_iff_isClosed,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ closure[inst✝] s = s
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
s : Set X
hs : IsDiscrete s
hf : IsInducing f
⊢ IsDiscrete (f '' s)

Tactic:
simp_all [isDiscrete_iff_nhdsWithin, ← hf.map_nhdsWithin_eq s]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z

Tactic:
have h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z := by
    rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.sdiff_union_of_subset, sUnion_irreducibleComponents]
    rwa [Set.singleton_subset_iff]
  apply Set.Subset.antisymm
  · rwa [(isClosed_of_mem_irreducibleComponents Z hZ).closure_subset_iff]
  · rw [← Set.inter_eq_right.mpr h]
    apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2
    · rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
      exact hX.sdiff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1
    · rw [Set.inter_compl_nonempty_iff]
      exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.sdiff Set.sdiff_subset)
        (Set.notMem_sdiff_of_mem (Set.mem_singleton Z))

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
⊢ a ∈ (U \ s)ᶜ

Tactic:
by_cases h₂a : a = x

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : a = x
⊢ a ∈ (U \ s)ᶜ

case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous continuous_isLeft <| by simp

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

Goal state before:
pp: case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous continuous_isLeft <| by simp

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
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
← hf.range_eq,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (range f)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
← hf.range_eq,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (range f)
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (n_1 : α),
    n ≤ n_1 →
      ((∀ i ∈ Ico n n_1, r i (succ i)) → ReflTransGen r n n_1) →
        (∀ i ∈ Ico n (succ n_1), r i (succ i)) → ReflTransGen r n (succ n_1)

Tactic:
intro m hnm ih h

Goal state after:
case refine_2
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
⊢ ReflTransGen r n (succ m)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}) ∧ ∀ᶠ (x_1 : X) in pure x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}

Tactic:
eventually_pure,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 ∈ s ∪ {x} ↔ x_1 ∈ t ∪ {x}) ∧ (x ∈ s ∪ {x} ↔ x ∈ t ∪ {x})
Module: Mathlib.Topology.Order.OrderClosed

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

Tactic:
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)

Goal state after:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ (Iic b)ᶜ ∈ 𝓝 a
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ IsOpen[inst✝] s ↔ frontier s = ∅

Tactic:
← closure_eq_iff_isClosed,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ IsOpen[inst✝] s ↔ frontier s = ∅
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
⊢ IsLindelof (f '' s)

Tactic:
intro l

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsLindelof s
hf : ContinuousOn f s
l : Filter Y
⊢ ∀ [l.NeBot] [CountableInterFilter l], l ≤ 𝓟 (f '' s) → ∃ x ∈ f '' s, ClusterPt x l
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
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (𝓝 b).HasBasis (?m.10 b) (?m.11 b)

Tactic:
rw [hf.nhds_eq_comap b]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (?m.10 b) (?m.11 b)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ i ∈ b, IsOpen[inst✝] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsLindelof s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen[inst✝] (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F

Tactic:
split_ifs <;> simp [connectedComponent_nonempty, *]

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
⊢ interior s = ∅

Tactic:
refine eq_empty_iff_forall_notMem.2 fun x hx => ?_

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 : x ∈ interior s
⊢ False
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
⊢ IsLindelof (insert y (range f))

Tactic:
intro l

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
⊢ ∀ [l.NeBot] [CountableInterFilter l], l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected v
⊢ (f '' v).Subsingleton

Tactic:
exact (hs v hvs hu).image _

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsConnected (⇑h ⁻¹' s) ↔ IsConnected s

Tactic:
rw [← image_symm, isConnected_image]

Goal state after: