mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
⊢ Tendsto (fun p ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
rw [frequently_iff_seq_frequently] at h

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
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 : α
n : ℤ
⊢ toIcoMod hp a (a + n • p) = a

Tactic:
rw [toIcoMod_add_zsmul, toIcoMod_apply_left]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ (∀ x ∈ x✝, 𝓝 x ≤ 𝓟 x✝) ↔ ∀ x ∈ x✝, 𝓝 x ≤ 𝓟 x✝

Tactic:
H

Goal state after:
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 : α
⊢ b - toIcoDiv hp a b • p = b - toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b

Tactic:
sub_right_inj,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p = toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b
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 : α
⊢ b - toIcoDiv hp a b • p = b - (toIocDiv hp a b • p + p) ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
sub_right_inj,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p = toIocDiv hp a b • p + p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
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✝ c : α
n : ℤ
a : α
b : α ⧸ AddSubgroup.zmultiples p
⊢ (fun x ↦ ↑↑x) ((fun b ↦ ⟨⋯.lift b, ⋯⟩) b) = b

Tactic:
by
    induction b using QuotientAddGroup.induction_on
    dsimp
    rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]
    apply AddSubgroup.zsmul_mem_zmultiples

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case right
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
rw [not_le] at h₁₂₃ h₂₃₄ ⊢
    exact (h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
isClosed_iff_clusterPt

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ MapClusterPt (f x) l f ↔ ClusterPt x l

Tactic:
delta MapClusterPt ClusterPt
  rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]

Goal state after:
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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.37

Tactic:
exact Continuous fun p : X × Y => f p.1 p.2

Goal state after:
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 ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.38

Tactic:
exact Continuous fun p : X × Y => f p.1 p.2

Goal state after:
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]
  exact nhdsWithin_le_of_mem h

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))

Tactic:
inf_right_comm

Goal state after:
ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ ((⨅ i ∈ I, comap (eval i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval i ⁻¹' s i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), comap (eval i) (𝓝 (x i)) =
    (⨅ i ∈ I, comap (fun x ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x ↦ x i) ⁻¹' s i)) ⊓
      ⨅ i, ⨅ (_ : i ∉ I), comap (fun x ↦ x i) (𝓝 (x i))
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
h : ∀ (t : Set β), IsOpen[inst✝] t → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst✝] t
u : Set α
u_open : IsOpen[inst✝¹] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen[inst✝¹] (u ∩ s)

Tactic:
apply IsOpen.inter u_open hs

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 → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst✝¹, inst✝] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝², inst✝] fun x ↦ f x y
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ f x y ∈ closure[inst✝] (closure[inst✝] u)

Tactic:
apply map_mem_closure (hf₁ x) hy fun b hb ↦ ?_

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst✝¹, inst✝] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝², inst✝] fun x ↦ f x y
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
b : Y
hb : b ∈ t
⊢ f x b ∈ closure[inst✝] 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 ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)

Tactic:
simp_rw [← continuousOn_univ]; exact continuousOn_prod_of_discrete_right

Goal state after:
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)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi s)

Tactic:
rw [pi_def]; exact hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case succ
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
⊢ ∃ m, accumulate s (n + 1) ⊆ s m

Tactic:
obtain ⟨k, hk⟩ := hd m (n + 1)

Goal state after:
case succ
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : (fun x1 x2 ↦ x1 ⊆ x2) (s m) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s (n + 1)) (s k)
⊢ ∃ m, accumulate s (n + 1) ⊆ s m
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
⊢ sᶜᶜ ∈ cobounded α ↔ IsCobounded s

Tactic:
isCobounded_def,

Goal state after:
α : Type u_2
x✝ : Bornology α
s : Set α
⊢ sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)

Tactic:
subset_compl_comm,

Goal state after:
α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ (f ⁻¹' t)ᶜ
⊢ IsBounded (f '' s)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} =
    generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}

Tactic:
refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)

Goal state after:
case intro.refine_1
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s} ⊆ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s},
    IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] s
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Filter α
h : ∀ (s : Set α), sᶜ ∉ f ↔ s ∈ f
hf : f = ⊥
⊢ False

Tactic:
simp [hf] at h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : FirstCountableTopology α
x : α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
g : ℕ → α
hg : Tendsto g atTop (𝓝 x ⊓ f)
⊢ ∃ ψ, Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
exact ⟨g, (tendsto_inf.1 hg).1, (tendsto_inf.1 hg).2⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.map f)

Tactic:
change Continuous (ULift.up ∘ f ∘ ULift.down)

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ f ∘ ULift.down)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
let t' := (fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ t }

Goal state after:
α : 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}
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case right
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
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝¹ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this✝ : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
exact this.neBot

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
⊢ ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s

Tactic:
refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ i ∈ t, U i
⊢ ⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ

Tactic:
subset_compl_comm,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ i ∈ t, U i
⊢ s ⊆ (⋂ i ∈ t, (U 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
hSF : ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F
⊢ False

Tactic:
choose! U hxU hSU hUF using hSF

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
⊢ False
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed (range mk)

Tactic:
by rw [range_mk]; exact isClosed_univ

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x

Tactic:
rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ u

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x✝ : X
hx : x✝ ∈ s
hxu : x✝ ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ v

Tactic:
all_goals
    rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst✝] {x}) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst✝] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Tactic:
simp only [← principal_singleton, disjoint_principal_right]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
⊢ U ∈ {U✝, u, v} → (t ∩ U).Nonempty

Tactic:
H

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
t S U✝ : Set X
hU' : IsOpen[inst✝] U✝
h₁ : U✝ ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U✝
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
U : Set X
H : U ∈ {U✝, u, v}
⊢ (t ∩ U).Nonempty
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False

Tactic:
H

Goal state after:
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 : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ False
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
⊢ s ∈ S → ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ s

Tactic:
H

Goal state after:
case mp.sInter
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
T : (s : Set α) → s ∈ S → Set (Set α)
Tg : ∀ (s : Set α) (a : s ∈ S), T s a ⊆ g
Tct : ∀ (s : Set α) (a : s ∈ S), (T s a).Countable
hT : ∀ (s : Set α) (a : s ∈ S), ⋂₀ T s a ⊆ s
s : Set α
H : s ∈ S
⊢ ⋂₀ ⋃ s, ⋃ (H : s ∈ S), T s H ⊆ s
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s✝
s : Set α
⊢ s ∈ S → s ∈ countableGenerate g

Tactic:
H

Goal state after:
case mpr
α : Type u_2
g : Set (Set α)
s✝ : Set α
S : Set (Set α)
Sg : S ⊆ g
Sct : S.Countable
hS : ⋂₀ S ⊆ s✝
s : Set α
H : s ∈ S
⊢ s ∈ countableGenerate g
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case right
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
lne : l.NeBot
inst✝ : CountableInterFilter l
ls : l ≤ 𝓟 (f '' s)
this✝¹ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this✝ : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
exact this.neBot

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x

Tactic:
regularSpace_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ {s : Set X} {a : X}, IsClosed[inst✝] s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)) ↔
    ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
(Lean.cdot
 (Lean.cdotTk "·")
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.rwSeq
     "rw"
     (Tactic.optConfig [])
     (Tactic.rwRuleSeq "[" [(Tactic.rwRule ["←"] `not_nonempty_iff_eq_empty)] "]")
     [(Tactic.location "at" (Tactic.locationHyp [`hsuv]))])
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hsuv)))
    ";"
    (Tactic.rwSeq
     "rw"
     (Tactic.optConfig [])
     (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.app `inter_comm [`u]))] "]")
     [(Tactic.location "at" (Tactic.locationHyp [`this]))])
    []
    (Tactic.simpa
     "simpa"
     []
     []
     (Tactic.simpaArgsRest
      (Tactic.optConfig [])
      []
      []
      [(Tactic.simpArgs
        "["
        [(Tactic.simpStar "*") "," (Tactic.simpLemma [] [] `or_imp) "," (Tactic.simpLemma [] [] `forall_and)]
        "]")]
      ["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.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst✝¹] s

Tactic:
by
  have h := (regularSpace_TFAE X).out 0 2
  exact h.mp ‹_› _ _

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

Goal state before:
pp: X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
⊢ ∃ n, IsOpen[inst✝²] n ∧ Disjoint (closure[inst✝²] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)

Goal state after:
X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed[inst✝²] s
t_cl : IsClosed[inst✝²] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
n : Set X
nna : n ∈ 𝓝 a
ncl : IsClosed[inst✝²] n
nsubkc : n ⊆ tᶜ
⊢ ∃ n, IsOpen[inst✝²] n ∧ Disjoint (closure[inst✝²] n) t ∧ (a ∈ s → a ∈ n)