mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ (𝓝[<] x).NeBot

Tactic:
refine (hx₁.prod hx₂).mono ?_

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ 𝓝[<] x.1 ×ˢ 𝓝[<] x.2 ≤ 𝓝[<] x
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ (𝓝[>] x).NeBot

Tactic:
refine (hx₁.prod hx₂).mono ?_

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ 𝓝[>] x.1 ×ˢ 𝓝[>] x.2 ≤ 𝓝[>] x
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a

Tactic:
rw [nhdsWithin_inter, inf_eq_right]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
x✝ : X × Y
a : X
b : Y
⊢ (a, b) ∈ interior (s ×ˢ t) ↔ (a, b) ∈ interior s ×ˢ interior t

Tactic:
simp only [mem_interior_iff_mem_nhds, mem_prod, prod_mem_nhds_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsOpenMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsOpen[inst✝] u
⊢ IsOpen[instTopologicalSpaceSubtype] ((fun x ↦ ⟨f x, ⋯⟩) '' u)

Tactic:
by
  convert! (hf u hu).preimage continuous_subtype_val
  exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
f : Y → X
hf : IsClosedMap f
hp : ∀ (x : Y), p (f x)
u : Set Y
hu : IsClosed[inst✝] u
⊢ IsClosed[instTopologicalSpaceSubtype] ((fun x ↦ ⟨f x, ⋯⟩) '' u)

Tactic:
by
  convert! (hf u hu).preimage continuous_subtype_val
  exact Set.ext fun _ ↦ exists_congr fun _ ↦ and_congr_right' Subtype.ext_iff

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : Set ↑s
⊢ map Subtype.val (𝓝ˢ t) = 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
by
  rw [IsInducing.subtypeVal.map_nhdsSet_eq, Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a).HasBasis (fun t ↦ t ∈ image2 (fun x1 x2 ↦ x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id

Tactic:
rw [nhds_inf (t₁ := t₁)]

Goal state after:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis (fun t ↦ t ∈ image2 (fun x1 x2 ↦ x1 ∩ x2) B₁ B₂ ∧ a ∈ t) id
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
⊢ Disjoint (accumulate s i) (s j)

Tactic:
apply disjoint_left.2 (fun x hx ↦ ?_)

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ accumulate s i
⊢ x ∉ s j
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ((fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i) ∧
    a i ∈ (fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i

Tactic:
simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
      exact (h1 i).choose_spec.2

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
⊢ (o ∩ range g).Nonempty

Tactic:
rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩

Goal state after:
case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
⊢ (o ∩ range g).Nonempty
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst✝] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ s ⊆ f ⁻¹' closure[inst✝] (f '' c)

Tactic:
exact hc.trans (closure_subset_preimage_closure_image hf)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst✝ i] (if ((↑s).pi U).Nonempty then univ else ∅)

Tactic:
if_pos h

Goal state after:
case neg
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst✝ i] univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
  refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
  exacts [inter_subset_right,
    (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,
    htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,
    fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
by
  obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
  refine ⟨_, ?_, notMem_sdiff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).sdiff_empty⟩
  exacts [((countable_ofPred_finite_subset hb₁).image _).mono sdiff_subset, rfl]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α
  by_cases! hn : t.Nonempty
  · obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn
    exact ⟨b, ht.2.2⟩
  · exact ⟨fun n => ∅, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι), Continuous[inst✝¹ i, instTopologicalSpaceSigma] fun a ↦ Sigma.map f₁ f₂ ⟨i, a⟩) ↔
    ∀ (i : ι), Continuous[inst✝¹ i, inst✝ (f₁ i)] (f₂ i)

Tactic:
by
    simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
refine hf.surjective.forall.2 fun x ↦ ?_
    rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩
    exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩

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

Goal state before:
pp: case pos
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
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∈ s
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
if_pos h

Goal state after:
case pos
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
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∈ s
⊢ IsCompact (n'' i)
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
t t' : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) = 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] t

Tactic:
simp [nhdsSetWithin, ← prod_inf_prod, hs.nhdsSet_prod_eq ht]

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
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact univ

Tactic:
by
    rw [← hf'.range_eq]
    exact isCompact_range hf

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ map mk (𝓝 x) = 𝓝 (mk x)

Tactic:
rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ map mk (𝓝 x) = 𝓝 (mk x)

Tactic:
by
  rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

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

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
· rw [Ne.nhdsWithin_compl_singleton hy]
    exact nhdsWithin_le_nhds

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
⊢ (∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x) → ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
hb

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
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
⊢ IsPreirreducible s

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.intro "intro" [`u `v `hu `hv `hu' `hv'])
  []
  (Tactic.simpa
   "simpa"
   []
   []
   (Tactic.simpaArgsRest
    (Tactic.optConfig [])
    []
    []
    [(Tactic.simpArgs "[" [(Tactic.simpStar "*")] "]")]
    ["using"
     (Term.app
      `h
      [(choice
        («term{_}» "{" [`u "," `v] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields
          [(Term.structInstField (Term.structInstLVal `u []) [])
           ","
           (Term.structInstField (Term.structInstLVal `v []) [])])
         (Term.optEllipsis [])
         []
         "}"))])]))])

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
⊢ IsOpen[inst✝] b → (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty

Tactic:
hb

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
⊢ (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y) ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y

Tactic:
simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

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

Tactic:
intro _
    exact ReflTransGen.refl

Goal state after:
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
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x

Tactic:
rwa [ContinuousAt, eq_of_tendsto_nhds h]

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

Goal state before:
pp: X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
⊢ R1Space X

Tactic:
by
  let _ := sInf T
  refine ⟨fun x y ↦ ?_⟩
  simp only [Specializes, nhds_sInf]
  by_cases! hTd : ∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)
  · rcases hTd with ⟨t, htT, htd⟩
    exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)
  · exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ map f l
⊢ ⋂₀ S ∈ map f l

Tactic:
simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter α
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, f ⁻¹' s ∈ l
⊢ ⋂ i ∈ S, f ⁻¹' i ∈ l
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case refine_1.inr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h : LocallyConnectedSpace ((i : ι) → X i)
x : (i : ι) → X i
this : ∀ (i : ι), Nonempty (X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ connectedComponent x
i : ι
hi : i ∈ {i | ¬PreconnectedSpace (X i)}
hiJ : i ∉ J
z : X i
x✝ : z ∈ univ
j : ι
hj : j ∈ J
⊢ x j ∈ t j

Tactic:
exact mem_of_mem_nhds (ht j)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
hsf : s ⊆ range f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
hsf : s ⊆ range f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty

Tactic:
replace hsf : f '' f ⁻¹' s = s := image_preimage_eq_of_subset hsf

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (f ⁻¹' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
⊢ y ∈ closure[inst✝¹] s

Tactic:
by_contra! hy'

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : y ∉ closure[inst✝¹] s
⊢ False
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
⊢ IsClosed[inst✝²] b → ⋂ s, ↑s ⊆ a ∪ b → Disjoint a b → ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
hb

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
⊢ ⋂ s, ↑s ⊆ a ∪ b → Disjoint a b → ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: case pos
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
h : j = i
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ ⋯ ▸ a.1

Tactic:
subst h
        exact continuous_fst

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf : IsInducing ⇑f
⊢ IsInducing (⇑(embedProduct N) ∘ ⇑(map f))

Tactic:
exact hf.prodMap (opHomeomorph.isInducing.comp <| hf.comp opHomeomorph.symm.isInducing)
    |>.comp isInducing_embedProduct

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

Goal state before:
pp: α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
⊢ b ∈ Prod.mk a ⁻¹' V → Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity

Tactic:
hb

Goal state after:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
⊢ Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift f

Tactic:
rw [lift_lift'_assoc]
      · exact monotone_id.relComp monotone_id
      · exact h

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

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

Tactic:
exact ⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| Nat.lt_add_one n).le⟩

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

Goal state before:
pp: case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
⊢ b ≥ N + k → (u a, u b) ∈ V

Tactic:
hb

Goal state after:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ (u a, u b) ∈ V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (univ ×ˢ univ)) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
univ_prod_univ,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 univ) (𝓤 β) ↔ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K

Tactic:
rwa [image_univ, range_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuousOn (↿f) (univ ×ˢ univ)

Tactic:
univ_prod_univ,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuousOn (↿f) univ