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

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s

Tactic:
intro h

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ⋃ t ∈ g '' S, f ⁻¹' t = ⋃₀ S

Tactic:
biUnion_image,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : Set X → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ⋃ y ∈ S, f ⁻¹' g y = ⋃₀ S
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 : α
⊢ toIcoDiv hp a b = toIcoDiv hp 0 (b - a)

Tactic:
rw [toIcoDiv_sub_eq_toIcoDiv_add, zero_add]

Goal state after:
Module: Mathlib.Topology.ClusterPt

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

Tactic:
have : (∃ᶠ z in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ z in 𝓝 x, z ∈ C ∧ z ∈ ({x} : Set X)ᶜ :=
    frequently_inf_principal.trans <| by simp only [and_comm]

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}ᶜ
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
intro h

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
⊢ x ∈ C ∨ AccPt x (𝓟 C)
Module: Mathlib.Topology.ClusterPt

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

Tactic:
intro h

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : pure x ≤ F.lift' closure[inst✝]
⊢ (pure x ⊓ F.lift' closure[inst✝]).NeBot
Module: Mathlib.Topology.ClusterPt

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

Tactic:
intro h

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
⊢ pure x ≤ F.lift' closure[inst✝]
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ ¬(𝓝ˢ s).NeBot ↔ ¬s.Nonempty

Tactic:
by simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
· rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩
    exact
      ⟨⟨fun _ ↦ U,
        h_sub_U.trans (iUnion_const U).symm.subset,
        fun _ ↦
          ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
       ⟨fun _ ↦ V,
        k_sub_V.trans (iUnion_const V).symm.subset,
        fun _ ↦
          ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure[inst✝] ((fun x ↦ ∅) x✝)) s

Tactic:
simp only [closure_empty, empty_disjoint]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x

Tactic:
simp only [discreteTopology_iff_isOpen_singleton,
    isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen[t] xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
simp only [preimage_compl, compl_inj_iff]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
⊢ induced ofTopology t = ⊤ → t = ⊤

Tactic:
intro h

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
h : induced ofTopology t = ⊤
⊢ t = ⊤
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t ↦ 𝓝 a) t

Tactic:
le_nhds_iff

Goal state after:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ IsCoinducing (g ∘ f) ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g

Tactic:
hf.isCoinducing.of_comp_iff,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ IsCoinducing g ∧ Surjective (g ∘ f) ↔ IsCoinducing g ∧ Surjective g
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst✝] (f '' s)
⊢ IsClosed[inst✝¹] s

Tactic:
rw [← preimage_image_eq s hf.injective]
    exact h.preimage hf.continuous

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x

Tactic:
rw [nhdsWithin, sdiff_eq, sdiff_eq, ← inf_principal, ← inf_assoc]
  exact inter_mem_inf hs (mem_principal_self _)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (s.domRestrict f) x) → ∀ x ∈ s, ContinuousWithinAt f s x

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
⊢ ∀ x ∈ s, ContinuousWithinAt f s x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) →
    ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
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
⊢ IsOpen[instTopologicalSpaceProd] (s ×ˢ t) ↔ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.1 h]
  · have st : s.Nonempty ∧ t.Nonempty := prod_nonempty_iff.1 h
    constructor
    · intro (H : IsOpen (s ×ˢ t))
      refine Or.inl ⟨?_, ?_⟩
      · simpa only [fst_image_prod _ st.2] using isOpenMap_fst _ H
      · simpa only [snd_image_prod st.1 t] using isOpenMap_snd _ H
    · intro H
      simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
      exact H.1.prod H.2

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
⊢ (∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)) →
    ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst✝¹] s
h : ∀ (t : Set β), IsOpen[inst✝] t → IsOpen[inst✝¹] (s ∩ f ⁻¹' t)
⊢ ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Prod.map f g)

Tactic:
by
  rw [isOpenMap_iff_nhds_le]
  rintro ⟨a, b⟩
  rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']
  exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

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

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f → (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)

Tactic:
intro h

Goal state after:
case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
h : IsClosedMap f
⊢ (IsClosedMap fun a ↦ f (inl a)) ∧ IsClosedMap fun b ↦ f (inr b)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : Continuous[inst✝¹, inst✝] f
⊢ ContinuousOn f s

Tactic:
← continuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous[inst✝², inst✝¹] f
hs : ∀ (x : α), f x ∈ s
⊢ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
← continuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, hvB', hxv, hvw⟩ := h w hwB x hxw

Goal state after:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
v : Set α
hvB' : v ∈ B'
hxv : x ∈ v
hvw : v ⊆ w
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (a : α), Continuous[inst✝², inst✝¹] fun x ↦ f (a, x)

Tactic:
← continuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x ↦ f (a, x)) univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)

Tactic:
← continuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) univ
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∀ (n : ℕ), s n ≠ univ) → ∀ (n : ℕ), accumulate s n ≠ univ

Tactic:
intro h

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
⊢ ∀ (n : ℕ), accumulate s n ≠ univ
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
⊢ x✝ ∈ V ∩ f ⁻¹' U → f x✝ ∈ U

Tactic:
intro h

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ f x✝ ∈ U
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ IsBounded (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsBounded s

Tactic:
isBounded_biUnion hs

Goal state after:
α : Type u_2
inst✝ : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ (∀ i ∈ S, IsBounded i) ↔ ∀ s ∈ S, IsBounded s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk x.fst) (𝓝 x.snd)

Tactic:
cases x

Goal state after:
case mk
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 ⟨fst✝, snd✝⟩ = Filter.map (mk ⟨fst✝, snd✝⟩.fst) (𝓝 ⟨fst✝, snd✝⟩.snd)
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ a_1 ∈ (fun x ↦ a ↑x) '' T, a_1

Tactic:
biUnion_image,

Goal state after:
case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ y ∈ T, a ↑y
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
by
  rw [tendsto_smallSets_iff]
  refine forall₂_congr fun u hu ↦ ?_
  rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]
  simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.smallSets = pure ∅

Tactic:
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]

Goal state after:
α : Type u_1
⊢ Monotone powerset
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ L ∈ 𝓝ˢ K

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
hi : i ∈ {i | y ∈ s i}
⊢ i ∈ {i | x ∈ s i}

Tactic:
push _ ∈ _ at hy

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
i : ι
hi : i ∈ {i | y ∈ s i}
hy : ∀ (i : ι), x ∉ s i → y ∉ s i
⊢ i ∈ {i | x ∈ s i}
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 π
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
    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
⊢ IsCompact (s ∩ t)

Tactic:
intro f hnf 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
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
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
⊢ False

Tactic:
have : ∀ s ∈ Q, s ∉ F := fun s hsQ ↦ (hQU hsQ).choose_spec.2 ▸ hUF _ (hQU hsQ).choose_spec.1

Goal state after:
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
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
⊢ False
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
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
⊢ y ∈ insert y✝ (range f) → y ∈ f '' K

Tactic:
hyf

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
hne : l.NeBot
hle : l ≤ 𝓟 (insert y✝ (range f))
s : Set Y
hsy : s ∈ 𝓝 y✝
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y✝ (range f)
⊢ y ∈ f '' K
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
⊢ Nontrivial (SeparationQuotient α) ↔ NontrivialTopology α

Tactic:
by
  simpa [not_subsingleton_iff_nontrivial] using subsingleton_iff.not

Goal state after:
Module: Mathlib.Topology.Piecewise

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

Tactic:
← continuousOn_univ

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

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

Tactic:
← continuousOn_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x) →
    ∀ (f : Ultrafilter ((i : ι) → X i)),
      {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
intro h

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
⊢ ∀ (f : Ultrafilter ((i : ι) → X i)),
    {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f → ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ ↑f → ∃ x ∈ s i, ↑f ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x | ∀ (i : ι), x i ∈ s i} ∈ ↑f
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval i) (↑f) (𝓝 (x i))
⊢ ∃ x ∈ {x | ∀ (i : ι), x i ∈ s i}, ∀ (i : ι), Tendsto (eval i) (↑f) (𝓝 (x i))

Tactic:
exact ⟨x, fun i => (hx i).left, fun i => (hx i).right⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) → ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
intro h

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
⊢ ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s) → ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t

Tactic:
intro h

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
⊢ ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
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 : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)

Tactic:
hf.nhds_le x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ map f (𝓝 x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)